Reference · Sets

rainbow.math.sets.image-certificates

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

Constructive image/target inclusions from certified set maps.

Depends onmath.sets.inverse-certificates

set/image-subset-of-maps-to.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (maps-evidence : set/maps-to A B mapping source target)
  → set/subset B (set/image A B mapping source) target

set/target-subset-image-of-surjective-on.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (surjection-evidence : set/surjective-on A B mapping source target)
  → set/subset B target (set/image A B mapping source)

set/image-target-equivalent-of-maps-surjective.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  (maps-evidence : set/maps-to A B mapping source target)
  (surjection-evidence : set/surjective-on A B mapping source target)
  → proposition/conjunction (subset) (subset₁)
  where subset := set/subset B (set/image A B mapping source) target
  where subset₁ := set/subset B target (set/image A B mapping source)

set/image-target-equivalent-of-bijective-on.{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)
  → proposition/conjunction (subset) (subset₁)
  where subset := set/subset B (set/image A B mapping source) target
  where subset₁ := set/subset B target (set/image A B mapping source)

set/image-target-equivalent-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)
  → proposition/conjunction (subset₁) (subset)
  where subset := set/subset B target (set/image A B forward source)
  where subset₁ := set/subset B (set/image A B forward source) target