coinduced_bot — Mathlib

English

The coinduced of the bottom topology along any map is the bottom topology: coinduced f ⊥ = ⊥.

Русский

Коиндуцированная по произвольному отображению нижняя топология сохраняется: коиндуцированная ⊥ по f равна ⊥.

LaTeX

$$$\operatorname{coinduced} f(\bot) = \bot$$$

Lean4

@[simp]
theorem coinduced_bot : (⊥ : TopologicalSpace α).coinduced f = ⊥ :=
  (gc_coinduced_induced f).l_bot

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