Reference · Sets

rainbow.math.sets.range-surjective

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

Characterize surjections by their universal ranges.

set/range-subset-universal

TheoremFor all inputsNo axiomsSource, line 38

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

set/universal-subset-range-of-surjective

TheoremFor all inputsNo axiomsSource, line 57

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

= = equality/Eq

set/range-universal-mutual-subset-of-surjective

TheoremFor all inputsNo axiomsSource, line 85

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

= = equality/Eq

function/surjective-equivalent-range-universal-mutual-subset

TheoremFor all inputsNo axiomsSource, line 120

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

= = equality/Eq