Reference · Sets

rainbow.math.sets.image-lattice

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

Images preserve unions, and preserve intersections under injectivity.

Depends onmath.finite.set

set/image-union-subset-union-images.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set A)
  → set/subset B (image) (union)
  where image := set/image A B mapping (set/union A left right)
  where union := set/union B (set/image A B mapping left) (set/image A B mapping right)

set/union-images-subset-image-union.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set A)
  → set/subset B (union) (image)
  where image := set/image A B mapping (set/union A left right)
  where union := set/union B (set/image A B mapping left) (set/image A B mapping right)

set/image-union-equivalent-union-images.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set A)
  → proposition/conjunction (subset) (subset₁)
  where subset := set/subset B (set/image A B mapping (set/union A left right)) (set/union B (set/image A B mapping left) (set/image A B mapping right))
  where subset₁ := set/subset B (set/union B (set/image A B mapping left) (set/image A B mapping right)) (set/image A B mapping (set/union A left right))

set/image-intersection-subset-intersection-images.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set A)
  → set/subset B (image) (intersection)
  where image := set/image A B mapping (set/intersection A left right)
  where intersection := set/intersection B (set/image A B mapping left) (set/image A B mapping right)

set/intersection-images-subset-image-intersection-of-injective.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set A)
  (injection-evidence : set/injective-on A B mapping (set/union A left right))
  → set/subset B (intersection) (image)
  where image := set/image A B mapping (set/intersection A left right)
  where intersection := set/intersection B (set/image A B mapping left) (set/image A B mapping right)

set/image-intersection-equivalent-intersection-images-of-injective.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set A)
  (injection-evidence : set/injective-on A B mapping (set/union A left right))
  → proposition/conjunction (subset₁) (subset)
  where subset := set/subset B (set/intersection B (set/image A B mapping left) (set/image A B mapping right)) (set/image A B mapping (set/intersection A left right))
  where subset₁ := set/subset B (set/image A B mapping (set/intersection A left right)) (set/intersection B (set/image A B mapping left) (set/image A B mapping right))