Reference · Sets

rainbow.math.sets.image-composition

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

The image of a composite map is the nested image, by mutual inclusion.

Depends onmath.finite.set

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

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

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

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

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

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