eq_empty_or_Ici — Mathlib

English

If s is an upper set in a well-founded order, then s = ∅ or s = Ici a for some a.

Русский

Пусть s — верхнее множество в хорошо основанном порядке; тогда s = ∅ или существует a, такое что s = Ici a.

LaTeX

$$$[\\text{WellFoundedLT }\\\\alpha] \\\\ (h : \\\\mathrm{IsUpperSet}(s)) \\\\to s = \\\\emptyset \\\\lor (\\\\exists a, s = \\\\mathrm{Ici}(a))$$$

Lean4

theorem eq_empty_or_Ici [WellFoundedLT α] (h : IsUpperSet s) : s = ∅ ∨ (∃ a, s = Set.Ici a) :=
  by
  refine or_iff_not_imp_left.2 fun ha ↦ ?_
  obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 ha
  exact ⟨_, Set.ext fun b ↦ ⟨wellFounded_lt.min_le, (h · <| wellFounded_lt.min_mem _ ⟨a, ha⟩)⟩⟩

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