map_id — Mathlib

English

The map induced by the identity order-homomorphism on lower-sets is the identity map on the corresponding continuous maps.

Русский

Отображение, индуцированное идентичным отображением порядка на нижних множествах, является тождественным отображением между соответствующими непрерывными отображениями.

LaTeX

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

Lean4

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

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