eq_univ_or_Ioi — Mathlib

English

In a well-founded order, an upper set is either all elements or an initial ray Ioi a.

Русский

В хорошо упорядоченном порядке верхнее множество либо всё множество, либо луч Ioi a.

LaTeX

$$$[\\text{WellFoundedGT }\\\\alpha] (h : \\\\mathrm{IsUpperSet}(s)) \\\\to s = \\\\mathrm{univ} \\\\lor (\\\\exists a, s = \\\\mathrm{Ioi}(a))$$$

Lean4

theorem eq_univ_or_Ioi [WellFoundedGT α] (h : IsUpperSet s) : s = .univ ∨ (∃ a, s = Set.Ioi a) :=
  IsLowerSet.eq_univ_or_Iio (α := αᵒᵈ) h

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