induced_const — Mathlib

English

Inducing by a constant map yields the top (discrete) topology: induced_const(t) = ⊤.

Русский

Индуцированная константной картой топология равна дискретной: induced_const(t) = ⊤.

LaTeX

$$$\operatorname{induced}_{c_x}(t) = \top$ where $(c_x)(\beta) = x$$$

Lean4

theorem induced_const [t : TopologicalSpace α] {x : α} : (t.induced fun _ : β => x) = ⊤ :=
  le_antisymm le_top (@continuous_const β α ⊤ t x).le_induced

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