ofCoreEq_toCore

Mathlib.Topology.UniformSpace.Defs

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

← MathLib Explorer

English

If t equals the topological space of the core, then ofCoreEq u.toCore t h equals u.

Русский

Если t равно топологическому пространству ядра, то ofCoreEq u.toCore t h равно u.

LaTeX

$$$\\text{ofCoreEq}_{\\text{given}}(u.toCore, t, h) = u$$$

Lean4

theorem ofCoreEq_toCore (u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace) :
    .ofCoreEq u.toCore t h = u :=
  UniformSpace.ext rfl

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

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

Разделы

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

Аффилиация

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