rainbow.math.finite.set-classical

list/finite-of-injective-enumerated-images

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 286

list/finite-of-injective-enumerated-images.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (enumeration : List B)
  (source : set/Set A) (injection : set/injective-on A B mapping source)
  (source-image-cover : ∀ (value : A), ∀ (member : source value), list/membership B enumeration (mapping value))
  → set/finite A source

List = data/List

set/finite-of-injection-maps-to

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 314

set/finite-of-injection-maps-to.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (maps : set/maps-to A B mapping source target)
  (injection : set/injective-on A B mapping source)
  (target-finite : set/finite B target)
  → set/finite A source

set/finite-of-finite-image

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 382

set/finite-of-finite-image.{u, v} :
  (A : Type u) (B : Type v) (source : set/Set A) (mapping : A → B)
  (image-finite : set/finite B (set/image A B mapping source))
  (injection : set/injective-on A B mapping source)
  → set/finite A source

set/finite-image-equivalence

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 410

set/finite-image-equivalence.{u, v} :
  (A : Type u) (B : Type v) (source : set/Set A) (mapping : A → B)
  (injection : set/injective-on A B mapping source)
  → proposition/conjunction (finite → set/finite A source) (set/finite A source → finite)
  where finite := set/finite B (set/image A B mapping source)

set/infinite-image-preserved

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 444

set/infinite-image-preserved.{u, v} :
  (A : Type u) (B : Type v) (source : set/Set A) (mapping : A → B)
  (injection : set/injective-on A B mapping source)
  (source-infinite : set/infinite A source)
  → set/infinite B (set/image A B mapping source)

set/infinite-image-equivalence

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 475

set/infinite-image-equivalence.{u, v} :
  (A : Type u) (B : Type v) (source : set/Set A) (mapping : A → B)
  (injection : set/injective-on A B mapping source)
  → proposition/conjunction (infinite → set/infinite A source) (set/infinite A source → infinite)
  where infinite := set/infinite B (set/image A B mapping source)

set/infinite-of-injection-maps-to

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 510

set/infinite-of-injection-maps-to.{u, v} :
  (A : Type u) (B : Type v) (source : set/Set A) (target : set/Set B) (mapping : A → B)
  (injection : set/injective-on A B mapping source)
  (maps : set/maps-to A B mapping source target)
  (source-infinite : set/infinite A source)
  → set/infinite B target

set/not-injective-on-infinite-finite-image

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 545

set/not-injective-on-infinite-finite-image.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  (source-infinite : set/infinite A source)
  (image-finite : set/finite B (set/image A B mapping source))
  (x₁ : set/injective-on A B mapping source)
  → proposition/falsity

set/bijective-finite-equivalence

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 581

set/bijective-finite-equivalence.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (bijection : set/bijective-on A B mapping source target)
  → proposition/conjunction (set/finite A source → set/finite B target) (set/finite B target → set/finite A source)

set/infinite-difference-finite

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 633

set/infinite-difference-finite.{u} :
  (A : Type u) (source removed : set/Set A) (source-infinite : set/infinite A source)
  (removed-finite : set/finite A removed)
  → set/infinite A (set/difference A source removed)

set/finite-preimage-under-injection

TheoremFor all inputsAxioms: sha256:2756c280e97f5c73b7f8ed1cdae9b3e0f2871720be7d82785b6b81ef1fb84366Source, line 694

set/finite-preimage-under-injection.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (target : set/Set B)
  (injection : set/injective-on A B mapping (set/preimage A B mapping target))
  (target-finite : set/finite B target)
  → set/finite A (set/preimage A B mapping target)