Reference · Sets

rainbow.math.sets.image-difference

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

Images preserve set difference exactly when witnesses cannot collide.

Depends onmath.finite.set

set/image-difference-subset-difference-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))
  → set/subset B (image) (difference)
  where difference := set/difference B (set/image A B mapping left) (set/image A B mapping right)
  where image := set/image A B mapping (set/difference A left right)

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

set/image-difference-equivalent-difference-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/image A B mapping (set/difference A left right)) (set/difference B (set/image A B mapping left) (set/image A B mapping right))
  where subset₁ := set/subset B (set/difference B (set/image A B mapping left) (set/image A B mapping right)) (set/image A B mapping (set/difference A left right))