leftInvOn_piecewise — Mathlib

English

Under suitable IsImage assumptions, the left inverse property holds for a piecewise combination of two maps.

Русский

При разумных предпосылках IsImage выполнено свойство левой инверсии для составного по частям отображения.

LaTeX

$$LeftInvOn( t.piecewise(e^{-1}, e'^{-1}), s.piecewise(e, e'), s.ite(e.source, e'.source) )$$

Lean4

theorem leftInvOn_piecewise {e' : OpenPartialHomeomorph X Y} [∀ 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) :=
  h.toPartialEquiv.leftInvOn_piecewise h'

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