English
If e maps s to t and e' maps s to t, then the piecewise map t.piecewise(e.symm, e'.symm) is a left inverse to s.piecewise(e, e') on the domain s ite e.source ∪ s ite e'.source.
Русский
Если e переводит s в t, а e' тоже переводит s в t, то кусочно заданная обратная карта образует левообратную к кусочно заданному отображению.
LaTeX
$$$\\forall e,e':\\mathrm{PartialEquiv}(\\alpha,\\beta)\\,,\\; s,t\\subseteq \\alpha,\\; (h:\\ e.IsImage\\,s\\,t)\\, (h':\\ e'.IsImage\\,s\\,t)\\Rightarrow \\text{LeftInvOn}(t.piecewise(e.symm,e'.symm))\\,(s.piecewise(e,e'))\\,(s\\,\\mathrm{ite}\\,\\,e.source\\,e'.source)$$$$
Lean4
theorem leftInvOn_piecewise {e' : PartialEquiv α β} [∀ i, Decidable (i ∈ s)] [∀ i, Decidable (i ∈ t)]
(h : e.IsImage s t) (h' : e'.IsImage s t) :
LeftInvOn (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source) :=
by
rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩)
· rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]
· rw [piecewise_eq_of_notMem _ _ _ hs, piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 hs), e'.left_inv he]
