Reference · Sets

rainbow.math.sets.preimage-composition

Setssrc/rainbow/math/sets/preimage_composition.clj0 definitions, 6 theorems

Identity and composition laws for set preimages.

Depends onmath.finite.set

set/preimage-identity-subset-source.{u} :
  (A : Type u) (source : set/Set A)
  → set/subset A (preimage) source
  where preimage := set/preimage A A (function/identity A) source

set/source-subset-preimage-identity.{u} :
  (A : Type u) (source : set/Set A)
  → set/subset A source (preimage)
  where preimage := set/preimage A A (function/identity A) source

set/preimage-identity-equivalent-source.{u} :
  (A : Type u) (source : set/Set A)
  → proposition/conjunction (subset) (subset₁)
  where subset := set/subset A (set/preimage A A (function/identity A) source) source
  where subset₁ := set/subset A source (set/preimage A A (function/identity A) source)

set/preimage-compose-subset-nested-preimage.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (target : set/Set C)
  → set/subset A (preimage) (preimage₁)
  where preimage := set/preimage A C (function/compose A B C outer inner) target
  where preimage₁ := set/preimage A B inner (set/preimage B C outer target)

set/nested-preimage-subset-preimage-compose.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (target : set/Set C)
  → set/subset A (preimage₁) (preimage)
  where preimage := set/preimage A C (function/compose A B C outer inner) target
  where preimage₁ := set/preimage A B inner (set/preimage B C outer target)

set/preimage-compose-equivalent-nested-preimage.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (target : set/Set C)
  → proposition/conjunction (subset₁) (subset)
  where subset := set/subset A (set/preimage A B inner (set/preimage B C outer target)) (set/preimage A C (function/compose A B C outer inner) target)
  where subset₁ := set/subset A (set/preimage A C (function/compose A B C outer inner) target) (set/preimage A B inner (set/preimage B C outer target))