exists_isGLB — Mathlib

English

A neighborhood basis at a point x can be taken as balls centered at x with radius 1/(n+1) for n ∈ ℕ.

Русский

Основание окрестностей точки x можно взять из шаров B(x, 1/(n+1)), n ∈ ℕ.

LaTeX

$$$ (\\\\mathcal{N} x).HasBasis (fun _ => True) (fun n: \\\\mathbb{N} => ball x (\\\\frac{1}{n+1})) $$$

Lean4

theorem exists_isGLB [ClosedIicTopology α] {s : Set α} (hs : IsCompact s) (ne_s : s.Nonempty) : ∃ x ∈ s, IsGLB s x :=
  (hs.exists_isLeast ne_s).imp (fun x (hx : IsLeast s x) => ⟨hx.1, hx.isGLB⟩)

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