map_id — Mathlib

English

For any K ∈ Compacts α, mapping by the identity gives back K: K.map id continuous_id = K.

Русский

Для любого K ∈ Compacts α отображение по тождественному отображению возвращает K: K.map id continuous_id = K.

LaTeX

$$$\\forall {\\alpha} [\\text{TopologicalSpace }\\alpha] (K : \\mathrm{Compacts}(\\alpha)),\\\\ (K.map id continuous_id) = K$$$

Lean4

@[simp]
theorem map_id (K : Compacts α) : K.map id continuous_id = K :=
  Compacts.ext <| Set.image_id _

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