Reference · Finite types, distributions and Markov chains

rainbow.math.finite.set-fiber

Finite types, distributions and Markov chains src/rainbow/math/finite/set_fiber.clj1 definitions, 4 theorems

Constructive finite fibers inside finite source sets.

set/fiber-within

set/fiber-within.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : B)
  → set/Set A

set/fiber-within-subset

TheoremFor all inputsNo axiomsSource, line 57

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

set/fiber-within-member-source

TheoremFor all inputsNo axiomsSource, line 81

set/fiber-within-member-source.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : B)
  (value : A) (member : set/fiber-within A B mapping source target value)
  → source value

set/fiber-within-mapping-equals

TheoremFor all inputsNo axiomsSource, line 107

set/fiber-within-mapping-equals.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : B)
  (value : A) (member : set/fiber-within A B mapping source target value)
  → mapping value = target

= = equality/Eq

set/finite-fiber-within

TheoremFor all inputsNo axiomsSource, line 133

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