English
For an open set s in α, s is a compact element of the lattice of opens iff the underlying set is compact in α.
Русский
Для открытого множества s верно: компактный элемент гомогенной решетки открытых множеств эквивалентен тому, что как множество оно компактно в α.
LaTeX
$$$\forall s:\ Opens(\alpha),\ CompleteLattice.IsCompactElement(s) \iff IsCompact( (s) )$$$
Lean4
@[simp]
theorem isCompactElement_iff (s : Opens α) : CompleteLattice.IsCompactElement s ↔ IsCompact (s : Set α) :=
by
rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]
refine ⟨?_, fun H ι U hU => ?_⟩
· introv H hU hU'
obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
refine ⟨t, Set.Subset.trans ht ?_⟩
rw [coe_finset_sup, Finset.sup_eq_iSup]
rfl
· obtain ⟨t, ht⟩ := H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
refine ⟨t, Set.Subset.trans ht ?_⟩
simp only [Set.iUnion_subset_iff]
change ∀ i ∈ t, U i ≤ t.sup U
exact fun i => Finset.le_sup
