map_id — Mathlib

English

The induced map on upper-set spaces corresponding to the identity order-homomorphism is the identity continuous map.

Русский

Отображение верхних множеств, связанное с тождественным отображением в исходном порядке, является тождественным непрерывным отображением.

LaTeX

$$$\\mathrm{Topology.WithUpperSet.map}(\\mathrm{OrderHom.id}) = \\mathrm{ContinuousMap.id}(\\mathrm{Topology.WithUpperSet}(\\alpha)).$$$

Lean4

@[simp]
theorem map_id : map (OrderHom.id : α →o α) = ContinuousMap.id _ :=
  rfl

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