English
Suppose eX, eX' : OpenPartialHomeomorph X X' and eY, eY' : OpenPartialHomeomorph Y Y'. If (eX.prod eY).source is nonempty, then equality of products eX.prod eY = eX'.prod eY' is equivalent to the pairwise equality eX = eX' and eY = eY'.
Русский
Пусть eX, eX' — частичные гомеоморфизмы между X и X', eY, eY' — между Y и Y'. Если source произведения не пустое, то равенство произведений эквивалентно попарному равенству факторов.
LaTeX
$$$ (eX .prod eY).source \neq \varnothing \;\Rightarrow\; (eX.prod eY = eX'.prod eY' \;\Leftrightarrow\; eX = eX' \wedge eY = eY') $$$
Lean4
theorem prod_eq_prod_of_nonempty {eX eX' : OpenPartialHomeomorph X X'} {eY eY' : OpenPartialHomeomorph Y Y'}
(h : (eX.prod eY).source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY' :=
by
obtain ⟨⟨x, y⟩, -⟩ := id h
haveI : Nonempty X := ⟨x⟩
haveI : Nonempty X' := ⟨eX x⟩
haveI : Nonempty Y := ⟨y⟩
haveI : Nonempty Y' := ⟨eY y⟩
simp_rw [OpenPartialHomeomorph.ext_iff, prod_apply, prod_symm_apply, prod_source, Prod.ext_iff,
Set.prod_eq_prod_iff_of_nonempty h, forall_and, Prod.forall, forall_const, and_assoc, and_left_comm]
