English
There is an order isomorphism between the space of monotone maps α →o β × γ and the product of spaces of monotone maps α →o β and α →o γ.
Русский
Существует упорядоченная изоморфизм между пространством монотонных отображений α →o (β × γ) и произведением пространств α →o β и α →o γ.
LaTeX
$$$ prodIso : (α \to^o β \times γ) \cong^o (α \to^o β) \times (α \to^o γ) $$$
Lean4
/-- Order isomorphism between the space of monotone maps to `β × γ` and the product of the spaces
of monotone maps to `β` and `γ`. -/
@[simps]
def prodIso : (α →o β × γ) ≃o (α →o β) × (α →o γ)
where
toFun f := (fst.comp f, snd.comp f)
invFun f := f.1.prod f.2
map_rel_iff' := forall_and.symm
