English
A constant map with open singleton source and target provides an OpenPartialHomeomorph structure from X to Y, mapping every input to a fixed b.
Русский
Константное отображение с открытыми одиночными множествами источника и мишени задаёт структуру OpenPartialHomeomorph: каждый элемент идёт в фиксированное b.
LaTeX
$$def const (ha : IsOpen { a }) (hb : IsOpen { b }) : OpenPartialHomeomorph X Y$$
Lean4
/-- This is `PartialEquiv.single` as an open partial homeomorphism: a constant map,
whose source and target are necessarily singleton sets.
-/
def const (ha : IsOpen { a }) (hb : IsOpen { b }) : OpenPartialHomeomorph X Y
where
toPartialEquiv := PartialEquiv.single a b
open_source := ha
open_target := hb
continuousOn_toFun := by simp
continuousOn_invFun := by simp
