eq_empty_or_Iic — Mathlib

English

If s is a lower set in a well-founded greater-than order, then s = ∅ or s = Iic a for some a.

Русский

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

LaTeX

$$$[\\text{WellFoundedGT }\\\\alpha] (h : \\\\mathrm{IsLowerSet}(s)) \\\\to s = \\\\emptyset \\\\lor (\\\\exists a, s = \\\\mathrm{Iic}(a))$$$

Lean4

theorem eq_empty_or_Iic [WellFoundedGT α] (h : IsLowerSet s) : s = ∅ ∨ (∃ a, s = Set.Iic a) :=
  IsUpperSet.eq_empty_or_Ici (α := αᵒᵈ) h

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