coinduced_id

Mathlib.Topology.Order

URI: https://scilib.ai/kg/mathlib#coinduced_id

English

Coinduced by the identity map yields the original topology: coinduced id(t) = t.

Русский

Коиндуцированная по тождественному отображению возвращает исходную топологию: coinduced id(t) = t.

LaTeX

$$$\operatorname{coinduced}_{\mathrm{id}}(t) = t$$$

Lean4

theorem coinduced_id [t : TopologicalSpace α] : t.coinduced id = t :=
  TopologicalSpace.ext rfl

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

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

Разделы

Аффилиация

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