English
Same as 208075, but with the swapped roles of the components in the hypothesis, yielding the same equivalence.
Русский
Аналогично 208075, но с поменяными ролями компонент в гипотезе, что приводит к той же эквивалентности.
LaTeX
$$$ (eX'.prod eY').source.Nonempty \Rightarrow (eX.prod eY = eX'.prod eY' \Leftrightarrow eX = eX' \wedge eY = eY') $$$
Lean4
/-- The product of a finite family of `OpenPartialHomeomorph`s. -/
@[simps! toPartialEquiv apply symm_apply source target]
def pi : OpenPartialHomeomorph (∀ i, X i) (∀ i, Y i)
where
toPartialEquiv := PartialEquiv.pi fun i => (ei i).toPartialEquiv
open_source := isOpen_set_pi finite_univ fun i _ => (ei i).open_source
open_target := isOpen_set_pi finite_univ fun i _ => (ei i).open_target
continuousOn_toFun :=
continuousOn_pi.2 fun i => (ei i).continuousOn.comp (continuous_apply _).continuousOn fun _f hf => hf i trivial
continuousOn_invFun :=
continuousOn_pi.2 fun i => (ei i).continuousOn_symm.comp (continuous_apply _).continuousOn fun _f hf => hf i trivial
