Reference · Finite types, distributions and Markov chains

rainbow.math.finite.set-fiber-decomposition

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

A finite source is the union of its fibers over its finite image.

Depends onmath.finite.set-fibermath.finite.set-indexed-union

set/source-subset-image-fiber-union.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  → set/subset A source (union)
  where union := set/restricted-indexed-union A B (set/image A B mapping source) (fun target => set/fiber-within A B mapping source target)

set/image-fiber-union-subset-source.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  → set/subset A (union) source
  where union := set/restricted-indexed-union A B (set/image A B mapping source) (fun target => set/fiber-within A B mapping source target)

set/image-fiber-union-decomposition.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  → proposition/conjunction (subset) (subset₁)
  where subset := set/subset A source (set/restricted-indexed-union A B (set/image A B mapping source) (fun target => set/fiber-within A B mapping source target))
  where subset₁ := set/subset A (set/restricted-indexed-union A B (set/image A B mapping source) (fun target => set/fiber-within A B mapping source target)) source

set/finite-image-fiber-union.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  (source-finite : set/finite A source)
  → set/finite A (union)
  where union := set/restricted-indexed-union A B (set/image A B mapping source) (fun target => set/fiber-within A B mapping source target)