isEmpty — Mathlib

English

If α is empty, then β is empty whenever there exists a surjective function f: α → β.

Русский

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

LaTeX

$$$ [IsEmpty(\alpha)] {f: \alpha \to \beta} (hf: f \text{ is surjective}) : \mathrm{IsEmpty}(\beta) $$$

Lean4

theorem isEmpty [IsEmpty α] {f : α → β} (hf : f.Surjective) : IsEmpty β :=
  ⟨fun y ↦
    let ⟨x, _⟩ := hf y;
    IsEmpty.false x⟩
    -- See note [instance argument order]

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