Reference · Sets

rainbow.math.sets.image-preimage-adjunction

Setssrc/rainbow/math/sets/image_preimage_adjunction.clj0 definitions, 3 theorems

The constructive image/preimage Galois connection for set inclusion.

Depends onmath.sets.image-certificates

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

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

set/image-subset-equivalent-source-subset-preimage.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  → proposition/conjunction (subset₁ → subset) (subset → subset₁)
  where subset := set/subset A source (set/preimage A B mapping target)
  where subset₁ := set/subset B (set/image A B mapping source) target