Reference · Sets

rainbow.math.sets.inverse-certificates

Setssrc/rainbow/math/sets/inverse_certificates.clj0 definitions, 5 theorems

Constructive injectivity, surjectivity, and bijectivity from set inverses.

Depends onmath.finite.set

set/injective-on-of-left-inverse.{u, v} :
  (A : Type u) (B : Type v) (forward : A → B) (backward : B → A) (source : set/Set A)
  (left-inverse : set/left-inverse-on A B backward forward source)
  → set/injective-on A B forward source

set/surjective-on-of-right-inverse.{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)
  (right-inverse : set/right-inverse-on A B backward forward target)
  → set/surjective-on A B forward source target

set/bijective-on-of-inverse.{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)
  → set/bijective-on A B forward source target

set/inverse-on-symmetric.{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)
  → set/inverse-on B A forward backward target source

set/inverse-on-compose.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (forward-one : A → B) (backward-one : B → A)
  (forward-two : B → C) (backward-two : C → B) (source : set/Set A) (middle : set/Set B)
  (target : set/Set C) (forward-one-maps : set/maps-to A B forward-one source middle)
  (backward-two-maps : set/maps-to C B backward-two target middle)
  (inverse-one-evidence : set/inverse-on A B backward-one forward-one source middle)
  (inverse-two-evidence : set/inverse-on B C backward-two forward-two middle target)
  → set/inverse-on A C (compose) (compose₁) source target
  where compose := function/compose C B A backward-one backward-two
  where compose₁ := function/compose A B C forward-two forward-one