Reference · Sets

rainbow.math.sets.inverse-unique-fiber

Sets src/rainbow/math/sets/inverse_unique_fiber.clj0 definitions, 4 theorems

Two-sided set inverses provide unique witnesses in every target fiber.

Depends onmath.sets.inverse-certificates math.sets.fiber-unique

set/inverse-on-has-unique-fibers

TheoremFor all inputsNo axiomsSource, line 60

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

set/inverse-on-backward-in-fiber

TheoremFor all inputsNo axiomsSource, line 102

set/inverse-on-backward-in-fiber.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B) (backward-maps : set/maps-to B A backward target source)
  (inverse-evidence : set/inverse-on A B backward forward source target) (value : B)
  (target-member : target value)
  → set/fiber-within A B forward source value (backward value)

set/inverse-on-fiber-member-equals-backward

TheoremFor all inputsNo axiomsSource, line 146

set/inverse-on-fiber-member-equals-backward.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B)
  (inverse-evidence : set/inverse-on A B backward forward source target) (value : B)
  (candidate : A)
  (candidate-fiber : set/fiber-within A B forward source value candidate)
  → candidate = backward value

= = equality/Eq

set/inverse-on-has-canonical-unique-fibers

TheoremFor all inputsNo axiomsSource, line 222

set/inverse-on-has-canonical-unique-fibers.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (target : set/Set B) (backward-maps : set/maps-to B A backward target source)
  (inverse-evidence : set/inverse-on A B backward forward source target) (value : B)
  (target-member : target value)
  → proposition/conjunction (within) (∀ (other : A), ∀ (other-evidence : set/fiber-within A B forward source value other), other = backward value)
  where within := set/fiber-within A B forward source value (backward value)

= = equality/Eq