isSupFiniteCompact — Mathlib

English

If α has IsSupClosedCompact, then there exists a WellFoundedGT α, i.e., a well-founded greater-than relation on α.

Русский

Если в α выполняется IsSupClosedCompact, то существует WellFoundedGT α, то есть выпукло-устойчивое отношение «больше» на α.

LaTeX

$$WellFoundedGT α$$

Lean4

theorem isSupFiniteCompact [WellFoundedGT α] : IsSupFiniteCompact α := fun s =>
  by
  let S := {x | ∃ t : Finset α, ↑t ⊆ s ∧ t.sup id = x}
  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := wellFounded_gt.has_min S ⟨⊥, ∅, by simp⟩
  refine ⟨t, ht₁, (sSup_le _ _ fun y hy => ?_).antisymm ?_⟩
  ·
    classical
    rw [eq_of_le_of_not_lt (Finset.sup_mono (t.subset_insert y))
        (hm _ ⟨insert y t, by simp [Set.insert_subset_iff, hy, ht₁]⟩)]
    simp
  · rw [Finset.sup_id_eq_sSup]
    exact sSup_le_sSup ht₁

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