type_eq_one_iff_unique — Mathlib

English

Specialized Quotient induction on ordinals: if C holds for all type-r instances, then it holds for o.

Русский

Специализированный вывод по эквивалентности ординалов: если свойство выполняется для всех типов-отношений r, то оно выполняется для o.

LaTeX

$$$\forall C : \mathrm{Ordinal} \to \mathrm{Prop}, (o : \mathrm{Ordinal}) \to (\forall (\alpha r) [IsWellOrder \alpha r], C(\mathrm{type}(r))) \rightarrow C(o)$$$

Lean4

@[simp]
theorem type_eq_one_iff_unique [IsWellOrder α r] : type r = 1 ↔ Nonempty (Unique α) :=
  ⟨fun h ↦
    let ⟨s⟩ := type_eq.1 h;
    ⟨s.toEquiv.unique⟩,
    fun ⟨_⟩ ↦ type_eq_one_of_unique r⟩

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