replaceTopology_eq

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#UniformSpace.replaceTopology_eq

← MathLib Explorer

English

If h is an equality of topologies, then replacing topology by h yields the same UniformSpace.

Русский

Если h есть равенство топологий, то замена топологии по h не меняет UniformSpace.

LaTeX

$$$u.replaceTopology(h) = u$$$

Lean4

theorem replaceTopology_eq {α : Type*} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace) :
    u.replaceTopology h = u :=
  UniformSpace.ext rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru