Reference · Sets

rainbow.math.sets.preimage-lattice

Setssrc/rainbow/math/sets/preimage_lattice.clj0 definitions, 9 theorems

Preimages preserve intersection, union, and difference by exact reuse.

Depends onmath.finite.set

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

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

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

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

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

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

set/preimage-difference-subset-difference-preimages.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set B)
  → set/subset A (preimage) (difference)
  where difference := set/difference A (set/preimage A B mapping left) (set/preimage A B mapping right)
  where preimage := set/preimage A B mapping (set/difference B left right)

set/difference-preimages-subset-preimage-difference.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (left right : set/Set B)
  → set/subset A (difference) (preimage)
  where difference := set/difference A (set/preimage A B mapping left) (set/preimage A B mapping right)
  where preimage := set/preimage A B mapping (set/difference B left right)

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