symm_piecewise — Mathlib

English

The inverse of a piecewise partial equivalence equals the piecewise of the inverses with swapped domains, under appropriate image conditions.

Русский

Обратная к блочной (piecewise) частичной эквивалентности равна блочной (piecewise) обратных функций со сменой областей определения при необходимых условиях образа.

LaTeX

$$$ (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm $$$

Lean4

theorem symm_piecewise (e e' : PartialEquiv α β) {s : Set α} {t : Set β} [∀ x, Decidable (x ∈ s)]
    [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) :
    (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm :=
  rfl

Похожие утверждения