rainbow.math.finite.set

list/product-map

DefinitionSource, line 654

list/product-map.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (mapping : A → B → C)
  (left-enumeration : List A) (right-enumeration : List B)
  → List C

List = data/List

list/membership-append-left

TheoremFor all inputsNo axiomsSource, line 277

list/membership-append-left.{u} :
  (A : Type u) (left right : List A) (value : A) (member : list/membership A left value)
  → list/membership A (list/append A left right) value

List = data/List

list/membership-append-right

TheoremFor all inputsNo axiomsSource, line 322

list/membership-append-right.{u} :
  (A : Type u) (left right : List A) (value : A)
  (member : list/membership A right value)
  → list/membership A (list/append A left right) value

List = data/List

list/cover-cons

TheoremFor all inputsNo axiomsSource, line 344

list/cover-cons.{u} :
  (A : Type u) (selected : A) (source : set/Set A) (enumeration : List A)
  (source-cover : ∀ (value : A), ∀ (member : source value), list/membership A enumeration value)
  (value : A) (member : set/insert A selected source value)
  → list/membership A (data/cons A selected enumeration) value

List = data/List

list/cover-append

TheoremFor all inputsNo axiomsSource, line 425

list/cover-append.{u} :
  (A : Type u) (left-source right-source : set/Set A)
  (left-enumeration right-enumeration : List A)
  (left-cover : ∀ (value : A), ∀ (member : left-source value), list/membership A left-enumeration value)
  (right-cover : ∀ (value : A), ∀ (member : right-source value), list/membership A right-enumeration value)
  (value : A) (member : set/union A left-source right-source value)
  → list/membership A (append) value
  where append := list/append A left-enumeration right-enumeration

List = data/List

set/finite-insert-preserved

TheoremFor all inputsNo axiomsSource, line 386

set/finite-insert-preserved.{u} :
  (A : Type u) (selected : A) (source : set/Set A) (source-finite : set/finite A source)
  → set/finite A (set/insert A selected source)

set/finite-union-preserved

TheoremFor all inputsNo axiomsSource, line 474

set/finite-union-preserved.{u} :
  (A : Type u) (left right : set/Set A) (left-finite : set/finite A left)
  (right-finite : set/finite A right)
  → set/finite A (set/union A left right)

set/finite-subset-preserved

TheoremFor all inputsNo axiomsSource, line 522

set/finite-subset-preserved.{u} :
  (A : Type u) (small large : set/Set A) (inclusion : set/subset A small large)
  (large-finite : set/finite A large)
  → set/finite A small

set/finite-insert-equivalence

TheoremFor all inputsNo axiomsSource, line 563

set/finite-insert-equivalence.{u} :
  (A : Type u) (source : set/Set A) (selected : A)
  → proposition/conjunction (finite → set/finite A source) (set/finite A source → finite)
  where finite := set/finite A (set/insert A selected source)

set/finite-union-equivalence

TheoremFor all inputsNo axiomsSource, line 611

set/finite-union-equivalence.{u} :
  (A : Type u) (left right : set/Set A)
  → proposition/conjunction (set/finite A (set/union A left right) → conjunction) (conjunction → set/finite A (set/union A left right))
  where conjunction := proposition/conjunction (set/finite A left) (set/finite A right)

list/membership-map

TheoremFor all inputsNo axiomsSource, line 756

list/membership-map.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (enumeration : List A) (value : A)
  (member : list/membership A enumeration value)
  → list/membership B (list/map A B mapping enumeration) (mapping value)

List = data/List

list/membership-product-map

TheoremFor all inputsNo axiomsSource, line 884

list/membership-product-map.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (mapping : A → B → C)
  (left-enumeration : List A) (right-enumeration : List B) (left-value : A)
  (left-member : list/membership A left-enumeration left-value) (right-value : B)
  (right-member : list/membership B right-enumeration right-value)
  → list/membership C (map) (mapping left-value right-value)
  where map := list/product-map A B C mapping left-enumeration right-enumeration

List = data/List

list/cover-image

TheoremFor all inputsNo axiomsSource, line 952

list/cover-image.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  (enumeration : List A)
  (source-cover : ∀ (value : A), ∀ (member : source value), list/membership A enumeration value)
  (value : B) (member : set/image A B mapping source value)
  → list/membership B (list/map A B mapping enumeration) value

List = data/List

set/finite-image-preserved

TheoremFor all inputsNo axiomsSource, line 1017

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

product/eta

TheoremFor all inputsNo axiomsSource, line 922

product/eta.{u, v} :
  (A : Type u) (B : Type v) (value : data/Product A B)
  → (fun value₁ => data/pair A B (product/first A B value₁) (product/second A B value₁) = value₁) value

= = equality/Eq

list/cover-image2

TheoremFor all inputsNo axiomsSource, line 1072

list/cover-image2.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (mapping : A → B → C) (left : set/Set A)
  (right : set/Set B) (left-enumeration : List A) (right-enumeration : List B)
  (left-cover : ∀ (value : A), ∀ (member : left value), list/membership A left-enumeration value)
  (right-cover : ∀ (value : B), ∀ (member : right value), list/membership B right-enumeration value)
  (value : C) (member : set/image2 A B C mapping left right value)
  → list/membership C (map) value
  where map := list/product-map A B C mapping left-enumeration right-enumeration

List = data/List

set/finite-image2-preserved

TheoremFor all inputsNo axiomsSource, line 1179

set/finite-image2-preserved.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (left : set/Set A) (right : set/Set B)
  (mapping : A → B → C) (left-finite : set/finite A left)
  (right-finite : set/finite B right)
  → set/finite C (set/image2 A B C mapping left right)

list/cover-product

TheoremFor all inputsNo axiomsSource, line 1244

list/cover-product.{u, v} :
  (A : Type u) (B : Type v) (left : set/Set A) (right : set/Set B)
  (left-enumeration : List A) (right-enumeration : List B)
  (left-cover : ∀ (value : A), ∀ (member : left value), list/membership A left-enumeration value)
  (right-cover : ∀ (value : B), ∀ (member : right value), list/membership B right-enumeration value)
  (value : data/Product A B) (member : set/product A B left right value)
  → list/membership (data/Product A B) (map) value
  where map := list/product-map A B (data/Product A B) (fun left₁ => fun right₁ => data/pair A B left₁ right₁) left-enumeration right-enumeration

List = data/List

set/finite-product-preserved

TheoremFor all inputsNo axiomsSource, line 1314

set/finite-product-preserved.{u, v} :
  (A : Type u) (B : Type v) (left : set/Set A) (right : set/Set B)
  (left-finite : set/finite A left) (right-finite : set/finite B right)
  → set/finite (data/Product A B) (set/product A B left right)

set/finite-of-surjection

TheoremFor all inputsNo axiomsSource, line 1368

set/finite-of-surjection.{u, v} :
  (A : Type u) (B : Type v) (source : set/Set A) (target : set/Set B) (mapping : A → B)
  (surjection : set/surjective-on A B mapping source target)
  (source-finite : set/finite A source)
  → set/finite B target

set/infinite-mono

TheoremFor all inputsNo axiomsSource, line 1400

set/infinite-mono.{u} :
  (A : Type u) (small large : set/Set A) (inclusion : set/subset A small large)
  (small-infinite : set/infinite A small)
  → set/infinite A large

set/infinite-of-image

TheoremFor all inputsNo axiomsSource, line 1427

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

set/finite-seq-preserved

TheoremFor all inputsNo axiomsSource, line 1463

set/finite-seq-preserved.{u, v} :
  (A : Type u) (B : Type v) (mapping-set : set/Set (A → B)) (input-set : set/Set A)
  (mappings-finite : set/finite (A → B) mapping-set)
  (inputs-finite : set/finite A input-set)
  → set/finite B (set/seq A B mapping-set input-set)

set/finite-of-preimage-under-surjection

TheoremFor all inputsNo axiomsSource, line 1538

set/finite-of-preimage-under-surjection.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (target : set/Set B)
  (preimage-finite : set/finite A (set/preimage A B mapping target))
  (surjection : ∀ (target₁ : B), proposition/existence A (fun source => mapping source = target₁))
  → set/finite B target

= = equality/Eq

set/finite-of-product-left

TheoremFor all inputsNo axiomsSource, line 1570

set/finite-of-product-left.{u, v} :
  (A : Type u) (B : Type v) (left : set/Set A) (right : set/Set B)
  (product-finite : set/finite (data/Product A B) (set/product A B left right))
  (right-nonempty : set/nonempty B right)
  → set/finite A left

set/finite-of-product-right

TheoremFor all inputsNo axiomsSource, line 1639

set/finite-of-product-right.{u, v} :
  (A : Type u) (B : Type v) (left : set/Set A) (right : set/Set B)
  (product-finite : set/finite (data/Product A B) (set/product A B left right))
  (left-nonempty : set/nonempty A left)
  → set/finite B right

set/infinite-product-left

TheoremFor all inputsNo axiomsSource, line 1704

set/infinite-product-left.{u, v} :
  (A : Type u) (B : Type v) (left : set/Set A) (right : set/Set B)
  (left-infinite : set/infinite A left) (right-nonempty : set/nonempty B right)
  → set/infinite (data/Product A B) (set/product A B left right)

set/infinite-product-right

TheoremFor all inputsNo axiomsSource, line 1732

set/infinite-product-right.{u, v} :
  (A : Type u) (B : Type v) (left : set/Set A) (right : set/Set B)
  (right-infinite : set/infinite B right) (left-nonempty : set/nonempty A left)
  → set/infinite (data/Product A B) (set/product A B left right)