English
If a is a least upper bound of s, and f is a filter with s ∈ f and NeBot (f ⊓ nhds a), then a is the least upper bound of s.
Русский
Если a является наименьшей верхней границей множества s, и фильтр f удовлетворяет s ∈ f и NeBot (f ⊓ nhds a), тогда a является наименьшей верхней границей s.
LaTeX
$$(a ∈ upperBounds s) ∧ (s ∈ f) ∧ NeBot (f ⊓ nhds a) → IsLUB s a$$
Lean4
theorem isLUB_of_mem_nhds {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ upperBounds s) (hsf : s ∈ f) [NeBot (f ⊓ 𝓝 a)] :
IsLUB s a :=
⟨hsa, fun b hb =>
not_lt.1 fun hba =>
have : s ∩ {a | b < a} ∈ f ⊓ 𝓝 a := inter_mem_inf hsf (IsOpen.mem_nhds (isOpen_lt' _) hba)
let ⟨_x, ⟨hxs, hxb⟩⟩ := Filter.nonempty_of_mem this
have : b < b := lt_of_lt_of_le hxb <| hb hxs
lt_irrefl b this⟩
