English
For two open partial homeomorphisms e and e' and a subset s of X, the inverse of the piecewise map equals the piecewise map built from the inverses on the swapped domain with frontier updates; i.e., Symmetric identity between piecewise maps and their inverses.
Русский
Для двух частичных открытых гомеоморфизмов e и e' и подмножества s, обратная часть кусочной карты равна карте кусочно составленной из обратных на swapped-доменах с обновлениями границы.
LaTeX
$$$ (e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s H.symm H'.symm (H.frontier.inter_eq_of_inter_eq_of_eqOn H'.frontier Hs Heq) (H.frontier.symm_eqOn_of_inter_eq_of_eqOn Hs Heq) $$$
Lean4
@[simp]
theorem symm_piecewise (e e' : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} [∀ x, Decidable (x ∈ s)]
[∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
(Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : EqOn e e' (e.source ∩ frontier s)) :
(e.piecewise e' s t H H' Hs Heq).symm =
e.symm.piecewise e'.symm t s H.symm H'.symm (H.frontier.inter_eq_of_inter_eq_of_eqOn H'.frontier Hs Heq)
(H.frontier.symm_eqOn_of_inter_eq_of_eqOn Hs Heq) :=
rfl
