nhds_basis_clopens — Mathlib

English

If Y is ultra uniform and f: X → Y is uniform inducing, then X is ultra uniform.

Русский

Если Y имеет ультра-однородность и f: X → Y — тождественный индуктивный переход, то X также ультра-однородно.

LaTeX

$$$[\text{IsUltraUniformity } Y] \Rightarrow \text{IsUltraUniformity } X$ under IsUniformInducing f$$

Lean4

theorem nhds_basis_clopens (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ IsClopen s) id :=
  by
  refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_
  · intro V ⟨hV, h_symm, h_trans⟩
    refine
      ⟨ball x V, ⟨?_, isClopen_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity _ h_symm h_trans hV⟩, le_rfl⟩
    exact mem_ball_self _ hV
  · rintro u ⟨hx, hu⟩
    simp [hu.right.mem_nhds_iff, hx]

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