English
In a ClosedIicTopology, every compact nonempty set s has a least element.
Русский
В ClosedIicTopology любая компактная непустая множество имеет наименьший элемент.
LaTeX
$$IsCompact s → s.Nonempty → ∃ x ∈ s, IsLeast s x$$
Lean4
theorem exists_isLeast [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x, IsLeast s x :=
by
haveI : Nonempty s := ne_s.to_subtype
suffices (s ∩ ⋂ x ∈ s, Iic x).Nonempty from ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩
rw [biInter_eq_iInter]
by_contra H
rw [not_nonempty_iff_eq_empty] at H
rcases
hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
(Monotone.directed_ge fun _ _ h => Iic_subset_Iic.mpr h) with
⟨x, hx⟩
exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩
