Reference · Sets

rainbow.math.sets.image-insert

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

Images commute constructively with inserting one source value.

Depends onmath.finite.set

set/image-insert-subset-insert-image.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (selected : A) (source : set/Set A)
  → set/subset B (image) (insert)
  where image := set/image A B mapping (set/insert A selected source)
  where insert := set/insert B (mapping selected) (set/image A B mapping source)

set/insert-image-subset-image-insert.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (selected : A) (source : set/Set A)
  → set/subset B (insert) (image)
  where image := set/image A B mapping (set/insert A selected source)
  where insert := set/insert B (mapping selected) (set/image A B mapping source)

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