Reference · Sets

rainbow.math.sets.fiber-characterization

Setssrc/rainbow/math/sets/fiber_characterization.clj0 definitions, 5 theorems

Image, surjection, and injection characterized by their source fibers.

Depends onmath.finite.set-fiber

set/fiber-nonempty-of-image-member.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : B)
  (image-member : set/image A B mapping source target)
  → set/nonempty A (within)
  where within := set/fiber-within A B mapping source target

set/image-member-of-fiber-nonempty.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : B)
  (fiber-nonempty : set/nonempty A (within))
  → set/image A B mapping source target
  where within := set/fiber-within A B mapping source target

set/image-member-equivalent-fiber-nonempty.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : B)
  → proposition/conjunction (set/image A B mapping source target → nonempty) (nonempty → set/image A B mapping source target)
  where nonempty := set/nonempty A (set/fiber-within A B mapping source target)

set/surjective-on-equivalent-nonempty-fibers.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A) (target : set/Set B)
  → proposition/conjunction (on → (∀ (value : B), ∀ (target-member : target value), set/nonempty A (set/fiber-within A B mapping source value))) ((∀ (value : B), ∀ (target-member : target value), set/nonempty A (set/fiber-within A B mapping source value)) → on)
  where on := set/surjective-on A B mapping source target

set/injective-on-equivalent-subsingleton-fibers.{u, v} :
  (A : Type u) (B : Type v) (mapping : A → B) (source : set/Set A)
  → proposition/conjunction (set/injective-on A B mapping source → (∀ (target : B), set/subsingleton A (set/fiber-within A B mapping source target))) ((∀ (target : B), set/subsingleton A (set/fiber-within A B mapping source target)) → set/injective-on A B mapping source)