Reference · Sets

rainbow.math.sets.range-image-bridge

Sets src/rainbow/math/sets/range_image_bridge.clj0 definitions, 4 theorems

Bridge global function ranges to images of universal source sets.

set/range-subset-image-universal

TheoremFor all inputsNo axiomsSource, line 37

set/range-subset-image-universal.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B)
  → set/subset B (set/range A B mapping) (set/image A B mapping (set/universal A))

set/image-universal-subset-range

TheoremFor all inputsNo axiomsSource, line 81

set/image-universal-subset-range.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B)
  → set/subset B (set/image A B mapping (set/universal A)) (set/range A B mapping)

set/range-equivalent-image-universal

TheoremFor all inputsNo axiomsSource, line 126

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

function/surjective-equivalent-universal-subset-range

TheoremFor all inputsNo axiomsSource, line 154

function/surjective-equivalent-universal-subset-range.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B)
  → proposition/conjunction ((∀ (target : B), proposition/existence A (fun source => mapping source = target)) → subset) (subset → (∀ (target : B), proposition/existence A (fun source => mapping source = target)))
  where subset := set/subset B (set/universal B) (set/range A B mapping)

= = equality/Eq