induced_id — Mathlib

English

Induced by the identity map leaves the topology unchanged: induced_id(t) = t.

Русский

Индуцированная идентичностью карта топологическую структуру не меняет: induced_id(t) = t.

LaTeX

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

Lean4

theorem induced_id [t : TopologicalSpace α] : t.induced id = t :=
  TopologicalSpace.ext <| funext fun s => propext <| ⟨fun ⟨_, hs, h⟩ => h ▸ hs, fun hs => ⟨s, hs, rfl⟩⟩

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