nonempty — Mathlib

English

If f : α → β is surjective and β is nonempty, then α is nonempty.

Русский

Если f : α → β сюръективно и β непусто, то α непусто.

LaTeX

$$$\forall {\alpha} {\beta} [h : \operatorname{Nonempty} \beta] {f : \alpha \to \beta}, \operatorname{Surjective} f \to \operatorname{Nonempty} \alpha$$$

Lean4

theorem nonempty [h : Nonempty β] {f : α → β} (hf : Function.Surjective f) : Nonempty α :=
  let ⟨y⟩ := h
  let ⟨x, _⟩ := hf y
  ⟨x⟩

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