to_nhds_mono — Mathlib

English

If u1 ≤ u2 for uniform spaces on α and a ∈ α, then nhds a in the topology of u1 is below nhds a in the topology of u2.

Русский

Если u1 ≤ u2 для равномерных структур на α и a ∈ α, то фильтр окрестностей a в топологии u1 лежит внутри фильтра окрестностей a в топологии u2.

LaTeX

$$nhds^{toTop(u1)}(a) ≤ nhds^{toTop(u2)}(a)$$

Lean4

theorem to_nhds_mono {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) (a : α) :
    @nhds _ (@UniformSpace.toTopologicalSpace _ u₁) a ≤ @nhds _ (@UniformSpace.toTopologicalSpace _ u₂) a := by
  rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]; exact lift'_mono h le_rfl

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