fst_surjective_iff — Mathlib

English

Let α be a type and β: α → Type be a family. Then the projection map fst: Σ a, β a → α is surjective if and only if every fiber β(a) is inhabited (nonempty).

Русский

Пусть α—тип, β : α → Type—семейство типов. Тогда отображение fst: Σ a, β a → α сюръективно тогда и только тогда, когда для каждого a ∈ α множество β(a) непусто.

LaTeX

$$$\\operatorname{Surjective}(\\operatorname{fst} : \\Sigma a:\\alpha, \\beta a \\to \\alpha) \\iff \\forall a:\\alpha, \\operatorname{Nonempty}(\\beta(a)).$$$

Lean4

theorem fst_surjective_iff : Surjective (fst : (Σ a, β a) → α) ↔ ∀ a, Nonempty (β a) :=
  ⟨fun h a ↦
    let ⟨x, hx⟩ := h a;
    hx ▸ ⟨x.2⟩,
    @fst_surjective _ _⟩

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