English
In a compactly generated lattice, for any a and s, a ∧ sSup s equals the supremum over all finite subsets t of s of a ∧ (sup t).
Русский
В компактно порождающейся решётке: для любых a и s, a ∧ sSup s равна наибольшему нижнему пределу по всем конечным подмножествам t ⊆ s: a ∧ (sup t).
LaTeX
$$$ a \wedge \operatorname{sSup} s = \bigvee_{t \subseteq s,\ t\text{ finite}} (a \wedge t.sup\, id) $$$
Lean4
/-- This property is equivalent to `α` being upper continuous. -/
theorem inf_sSup_eq_iSup_inf_sup_finset : a ⊓ sSup s = ⨆ (t : Finset α) (_ : ↑t ⊆ s), a ⊓ t.sup id :=
le_antisymm
(by
rw [le_iff_compact_le_imp]
intro c hc hcinf
rw [le_inf_iff] at hcinf
rcases hc s hcinf.2 with ⟨t, ht1, ht2⟩
refine (le_inf hcinf.1 ht2).trans (le_trans ?_ (le_iSup₂ t ht1))
rfl)
(iSup_le fun t => iSup_le fun h => inf_le_inf_left _ ((Finset.sup_id_eq_sSup t).symm ▸ sSup_le_sSup h))
