English
For a directed set s, a ⊓ sSup s equals ⨆ b ∈ s, a ⊓ b.
Русский
Для направленного множества s выполняется a ∧ sSup s = ⨆ b ∈ s, a ∧ b.
LaTeX
$$inf_sSup_eq (h : DirectedOn (≤) s) : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b$$
Lean4
/-- This property is sometimes referred to as `α` being upper continuous. -/
theorem inf_sSup_eq (h : DirectedOn (· ≤ ·) s) : a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b :=
le_antisymm
(by
rw [le_iff_compact_le_imp]
by_cases hs : s.Nonempty
· intro c hc hcinf
rw [le_inf_iff] at hcinf
rw [CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le] at hc
rcases hc s hs h hcinf.2 with ⟨d, ds, cd⟩
refine (le_inf hcinf.1 cd).trans (le_trans ?_ (le_iSup₂ d ds))
rfl
· rw [Set.not_nonempty_iff_eq_empty] at hs
simp [hs])
iSup_inf_le_inf_sSup
