toTopologicalSpace_inf — Mathlib

English

The topology of the infimum of two uniform spaces is the infimum of their topologies.

Русский

Топология инфимума двух равномерных пространств равна инфимуму их топологий.

LaTeX

$$(u ⊓ v).toTopologicalSpace = u.toTopologicalSpace ⊓ v.toTopologicalSpace$$

Lean4

theorem toTopologicalSpace_inf {u v : UniformSpace α} :
    (u ⊓ v).toTopologicalSpace = u.toTopologicalSpace ⊓ v.toTopologicalSpace :=
  rfl

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