English
The symmetry (inverse) of a product is the product of the symms: (eX.prod eY).symm = eX.symm.prod eY.symm.
Русский
Обратное к произведению равняется произведению обратных: (eX.prod eY).symm = eX.symm.prod eY.symm.
LaTeX
$$$ (eX.prod eY).symm = eX.symm.prod eY.symm $$$
Lean4
/-- The product of two open partial homeomorphisms, as an open partial homeomorphism on the product
space. -/
@[simps! (attr := mfld_simps) -fullyApplied toPartialEquiv apply, simps! -isSimp source target symm_apply]
def prod (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : OpenPartialHomeomorph (X × Y) (X' × Y')
where
open_source := eX.open_source.prod eY.open_source
open_target := eX.open_target.prod eY.open_target
continuousOn_toFun := eX.continuousOn.prodMap eY.continuousOn
continuousOn_invFun := eX.continuousOn_symm.prodMap eY.continuousOn_symm
toPartialEquiv := eX.toPartialEquiv.prod eY.toPartialEquiv
