toTopologicalSpace_mono — Mathlib

English

If u1 ≤ u2, then the induced topologies satisfy T(u1) ≤ T(u2).

Русский

Если u1 ≤ u2, то индуцированные топологии удовлетворяют T(u1) ≤ T(u2).

LaTeX

$$toTopologicalSpace u1 ≤ toTopologicalSpace u2$$

Lean4

theorem toTopologicalSpace_mono {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) :
    @UniformSpace.toTopologicalSpace _ u₁ ≤ @UniformSpace.toTopologicalSpace _ u₂ :=
  le_of_nhds_le_nhds <| to_nhds_mono h

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