fst_surjective — Mathlib

English

If β is nonempty, the first projection fst: α × β → α is surjective.

Русский

Если β непусто, проекция fst: α × β → α сюръективна.

LaTeX

$$$[h : Nonempty \\\\beta] \\\\Rightarrow \\\\operatorname{Surjective}(\\\\operatorname{fst}) \\\\text{, i.e. } \\\\forall a \\\\in \\\\alpha, \\\\exists b \\\\in \\\\beta, \\\\operatorname{fst}(a,b) = a.$$$

Lean4

theorem fst_surjective [h : Nonempty β] : Function.Surjective (@fst α β) := fun x ↦ h.elim fun y ↦ ⟨⟨x, y⟩, rfl⟩

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