toTopologicalSpace_comap — Mathlib

English

The topology on α induced by the comap of f from u equals the induced topology along f of the topology on β.

Русский

Топология на α, индуцированная обратным образом по f от u, равна топологии, индуцированной f от топологии β.

LaTeX

$$toTopologicalSpace(UniformSpace.comap f u) = TopologicalSpace.induced f (toTopologicalSpace u)$$

Lean4

theorem toTopologicalSpace_comap {f : α → β} {u : UniformSpace β} :
    @UniformSpace.toTopologicalSpace _ (UniformSpace.comap f u) =
      TopologicalSpace.induced f (@UniformSpace.toTopologicalSpace β u) :=
  rfl

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