nhds_basis_balanced — Mathlib

English

If U is closed and 0 ∈ U, then balancedCore 𝕜 U is closed (under suitable regularity conditions).

Русский

Если U замкнуто и 0 ∈ U, то balancedCore 𝕜 U замкнуто при подходящих условиях RegularSpace.

LaTeX

$$$(IsClosed\\ U) \\Rightarrow IsClosed (balancedCore\\ 𝕜\\ U)$$$

Lean4

theorem nhds_basis_balanced : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ Balanced 𝕜 s) id :=
  Filter.hasBasis_self.mpr fun s hs =>
    ⟨balancedCore 𝕜 s, balancedCore_mem_nhds_zero hs, balancedCore_balanced s, balancedCore_subset s⟩

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