type_eq_zero_iff_isEmpty — Mathlib

English

type r = 0 if and only if α is empty, given a well-order on α.

Русский

type r = 0 тогда и только тогда, когда α пусто, при условии существования упорядочения.

LaTeX

$$$\mathrm{type}(r) = 0 \iff \text{IsEmpty}(\alpha)$$$

Lean4

@[simp]
theorem type_eq_zero_iff_isEmpty [IsWellOrder α r] : type r = 0 ↔ IsEmpty α :=
  ⟨fun h =>
    let ⟨s⟩ := type_eq.1 h
    s.toEquiv.isEmpty,
    @type_eq_zero_of_empty α r _⟩

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