induced_top

Mathlib.Topology.Order

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

English

Let g: β → α. The topology on β induced by g from the topology ⊤ on α equals ⊤ on β.

Русский

Пусть g: β → α. Топология на β, индуцированная по g из топологии ⊤ на α, равна ⊤ на β.

LaTeX

$$$\operatorname{induced}_g(\top) = \top$$$

Lean4

@[simp]
theorem induced_top : (⊤ : TopologicalSpace α).induced g = ⊤ :=
  (gc_coinduced_induced g).u_top

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

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

Разделы

Аффилиация

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