Reference · Sets

rainbow.math.sets.fiber-unique

Sets src/rainbow/math/sets/fiber_unique.clj0 definitions, 5 theorems

Unique existence from subsingleton predicates, applied to bijection fibers.

Depends onmath.sets.fiber-characterization

proposition/unique-existence-of-existence-and-subsingleton

TheoremFor all inputsNo axiomsSource, line 33

proposition/unique-existence-of-existence-and-subsingleton.{u} :
  (A : Type u) (predicate : A → Prop)
  (some-evidence : proposition/existence A predicate)
  (subsingleton-evidence : ∀ (left : A), ∀ (left-evidence : predicate left), ∀ (right : A), ∀ (right-evidence : predicate right), left = right)
  → proposition/unique-existence A predicate

= = equality/Eq

proposition/existence-and-subsingleton-of-unique-existence

TheoremFor all inputsNo axiomsSource, line 65

proposition/existence-and-subsingleton-of-unique-existence.{u} :
  (A : Type u) (predicate : A → Prop)
  (unique-evidence : proposition/unique-existence A predicate)
  → proposition/conjunction (proposition/existence A predicate) (∀ (left : A), ∀ (left-evidence : predicate left), ∀ (right : A), ∀ (right-evidence : predicate right), left = right)

= = equality/Eq

proposition/unique-existence-equivalent-existence-and-subsingleton

TheoremFor all inputsNo axiomsSource, line 110

proposition/unique-existence-equivalent-existence-and-subsingleton.{u} :
  (A : Type u) (predicate : A → Prop)
  → proposition/conjunction (existence → conjunction) (conjunction → existence)
  where conjunction := proposition/conjunction (proposition/existence A predicate) (∀ (left : A), ∀ (left-evidence : predicate left), ∀ (right : A), ∀ (right-evidence : predicate right), left = right)
  where existence := proposition/unique-existence A predicate

= = equality/Eq

set/bijective-on-has-unique-fibers

TheoremFor all inputsNo axiomsSource, line 169

set/bijective-on-has-unique-fibers.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (bijection-evidence : set/bijective-on A B mapping source target) (value : B)
  (target-member : target value)
  → proposition/unique-existence A (within)
  where within := set/fiber-within A B mapping source value

set/bijective-on-equivalent-maps-to-and-unique-fibers

TheoremFor all inputsNo axiomsSource, line 247

set/bijective-on-equivalent-maps-to-and-unique-fibers.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  → proposition/conjunction (on → conjunction) (conjunction → on)
  where conjunction := proposition/conjunction (set/maps-to A B mapping source target) (∀ (value : B), ∀ (target-member : target value), proposition/unique-existence A (set/fiber-within A B mapping source value))
  where on := set/bijective-on A B mapping source target