English
The product of two partial equivalences yields a partial equivalence on the product types, with componentwise action.
Русский
Произведение двух частичных эквивалентностей даёт частичную эквивалентность на произведении множеств, действующую по компонентам.
LaTeX
$$$ \\text{prod}(e,e') : \\text{PartialEquiv}(\\alpha \\times \\gamma, \\beta \\times \\delta) $ with $\\mathrm{source}(\\text{prod}(e,e')) = \\mathrm{source}(e) \\times \\mathrm{source}(e'), \\mathrm{target}(\\text{prod}(e,e')) = \\mathrm{target}(e) \\times \\mathrm{target}(e') $ and appropriate maps defined componentwise.$$
Lean4
/-- The product of two partial equivalences, as a partial equivalence on the product. -/
def prod (e : PartialEquiv α β) (e' : PartialEquiv γ δ) : PartialEquiv (α × γ) (β × δ)
where
source := e.source ×ˢ e'.source
target := e.target ×ˢ e'.target
toFun p := (e p.1, e' p.2)
invFun p := (e.symm p.1, e'.symm p.2)
map_source' p hp := by simp_all
map_target' p hp := by simp_all
left_inv' p hp := by simp_all
right_inv' p hp := by simp_all
