eq_univ_or_Iio — Mathlib

English

In a well-founded order, a lower set is either everything or an initial segment Iio a.

Русский

В хорошо основанном порядке нижнее множество либо все множество, либо начальный оконный отрезок Iio a.

LaTeX

$$$[\\text{WellFoundedLT }\\\\alpha] (h : \\\\mathrm{IsLowerSet}(s)) \\\\to s = \\\\mathrm{univ} \\\\lor (\\\\exists a, s = \\\\mathrm{Iio}(a))$$$

Lean4

theorem eq_univ_or_Iio [WellFoundedLT α] (h : IsLowerSet s) : s = .univ ∨ (∃ a, s = Set.Iio a) :=
  by
  simp_rw [← @compl_inj_iff _ s]
  simpa using h.compl.eq_empty_or_Ici

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