surjective — Mathlib

English

The surjectivity of the map from sections Mk to the bottom object is ensured, i.e., every bottom element is hit by Mk.

Русский

Сюръективность отображения из sections Mk на нижний объект гарантируется.

LaTeX

$$$\\text{surjective}$$$

Lean4

theorem surjective : Function.Surjective ((fun s ↦ s (op ⊥)) ∘ Subtype.val : F.sections → F.obj (op ⊥)) := fun val₀ ↦
  ⟨d.sectionsMk val₀, d.sectionsMk_val_op_bot val₀⟩

Похожие утверждения