induced_eq

Mathlib.Topology.Homeomorph.Defs

URI: https://scilib.ai/kg/mathlib#Homeomorph.induced_eq

English

The coinduced topology on X via h equals the given topology on X.

Русский

Коиндуцированная топология на X через h равна данной топологии на X.

LaTeX

$$$\\operatorname{Coinduced}_h(\\mathcal{T}_Y) = \\mathcal{T}_X$$$

Lean4

theorem induced_eq (h : X ≃ₜ Y) : TopologicalSpace.induced h ‹_› = ‹_› :=
  h.isInducing.1.symm

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

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

Разделы

Аффилиация

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