English
If k is compact and s is a nonempty directed set with every element x < k, then sSup(s) < k.
Русский
Если k компактен и s — ненулево направленное множество, все элементы которого меньше k, то sSup(s) < k.
LaTeX
$$CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt hk hemp hdir hbelow$$
Lean4
/-- A compact element `k` has the property that any directed set lying strictly below `k` has
its `sSup` strictly below `k`. -/
theorem directed_sSup_lt_of_lt {α : Type*} [CompleteLattice α] {k : α} (hk : IsCompactElement k) {s : Set α}
(hemp : s.Nonempty) (hdir : DirectedOn (· ≤ ·) s) (hbelow : ∀ x ∈ s, x < k) : sSup s < k :=
by
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
by_contra h
have sSup' : sSup s ≤ k := sSup_le s k fun s hs => (hbelow s hs).le
replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le
obtain hxk := hbelow x hxs
exact hxk.ne (hxk.le.antisymm hkx)
