English
Let α and β be topological spaces endowed with a preorder. The collection of continuous order-preserving maps α →Co β carries a function-like structure in which equality is determined by the underlying function: if two elements have identical values at every input, they are equal.
Русский
Пусть α и β — топологические пространства с заданным порядком. Множество непрерывно упорядоченных отображений α →Co β образует структуру, в которой равенство элементов определяется их значениями на всех аргументах: если для всех аргументов значения совпадают, отображения равны.
LaTeX
$$$\forall f,g : \alpha \toCo \beta,\; f.toFun = g.toFun \Rightarrow f = g$$$
Lean4
instance instFunLike : FunLike (α →Co β) α β where
coe f := f.toFun
coe_injective' f g
h := by
obtain ⟨⟨_, _⟩, _⟩ := f
obtain ⟨⟨_, _⟩, _⟩ := g
congr
