isGLB_of_mem_nhds — Mathlib

English

If a is a greatest lower bound of s, and s ∈ f with a neighborhood filter intersecting f nontrivially, then a is the GLB of s.

Русский

Если a является наибольшей нижней границей множества s, и s принадлежит фильтру f при условии ненулевого пересечения f и nhds a, тогда a является ГЛБ множества s.

LaTeX

$$(a ∈ lowerBounds s) ∧ (s ∈ f) ∧ NeBot (f ⊓ nhds a) → IsGLB s a$$

Lean4

theorem isGLB_of_mem_nhds {s : Set α} {a : α} {f : Filter α} (hsa : a ∈ lowerBounds s) (hsf : s ∈ f) [NeBot (f ⊓ 𝓝 a)] :
    IsGLB s a :=
  isLUB_of_mem_nhds (α := αᵒᵈ) hsa hsf

Похожие утверждения