Reference · Finite types, distributions and Markov chains

rainbow.math.finite.set-image2-infinite

Finite types, distributions and Markov chainssrc/rainbow/math/finite/set_image2_infinite.clj0 definitions, 4 theorems

Infinitude transport through binary images and Cartesian products.

set/infinite-image2-left.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (mapping : A → B → C) (left : set/Set A)
  (right : set/Set B) (selected-right : B) (left-infinite : set/infinite A left)
  (selected-member : right selected-right)
  (injection : set/injective-on A C (fun left-value => mapping left-value selected-right) left)
  → set/infinite C (set/image2 A B C mapping left right)

set/infinite-image2-right.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (mapping : A → B → C) (left : set/Set A)
  (right : set/Set B) (selected-left : A) (right-infinite : set/infinite B right)
  (selected-member : left selected-left)
  (injection : set/injective-on B C (fun right-value => mapping selected-left right-value) right)
  → set/infinite C (set/image2 A B C mapping left right)

set/infinite-image2-equivalence.{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-injections : ∀ (selected-right : B), ∀ (selected-member : right selected-right), set/injective-on A C (fun left-value => mapping left-value selected-right) left)
  (right-injections : ∀ (selected-left : A), ∀ (selected-member : left selected-left), set/injective-on B C (fun right-value => mapping selected-left right-value) right)
  → proposition/conjunction (infinite → disjunction) (disjunction → infinite)
  where disjunction := proposition/disjunction (proposition/conjunction (set/infinite A left) (set/nonempty B right)) (proposition/conjunction (set/infinite B right) (set/nonempty A left))
  where infinite := set/infinite C (set/image2 A B C mapping left right)

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