Reference · Sets

rainbow.math.sets.map-composition

Setssrc/rainbow/math/sets/map_composition.clj0 definitions, 8 theorems

Constructive set-map properties preserved by function composition.

Depends onmath.finite.set

set/maps-to-identity.{u} :
  (A : Type u) (source : set/Set A)
  → set/maps-to A A (function/identity A) source source

set/injective-on-identity.{u} :
  (A : Type u) (source : set/Set A)
  → set/injective-on A A (function/identity A) source

set/surjective-on-identity.{u} :
  (A : Type u) (source : set/Set A)
  → set/surjective-on A A (function/identity A) source source

set/bijective-on-identity.{u} :
  (A : Type u) (source : set/Set A)
  → set/bijective-on A A (function/identity A) source source

set/maps-to-compose.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (source : set/Set A) (middle : set/Set B) (target : set/Set C)
  (inner-maps : set/maps-to A B inner source middle)
  (outer-maps : set/maps-to B C outer middle target)
  → set/maps-to A C (function/compose A B C outer inner) source target

set/injective-on-compose.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (source : set/Set A) (middle : set/Set B)
  (inner-maps : set/maps-to A B inner source middle)
  (inner-injective : set/injective-on A B inner source)
  (outer-injective : set/injective-on B C outer middle)
  → set/injective-on A C (function/compose A B C outer inner) source

set/surjective-on-compose.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (source : set/Set A) (middle : set/Set B) (target : set/Set C)
  (inner-surjective : set/surjective-on A B inner source middle)
  (outer-surjective : set/surjective-on B C outer middle target)
  → set/surjective-on A C (function/compose A B C outer inner) source target

set/bijective-on-compose.{u, v, w} :
  (A : Type u) (B : Type v) (C : Type w) (inner : A → B) (outer : B → C)
  (source : set/Set A) (middle : set/Set B) (target : set/Set C)
  (inner-bijective : set/bijective-on A B inner source middle)
  (outer-bijective : set/bijective-on B C outer middle target)
  → set/bijective-on A C (function/compose A B C outer inner) source target