symm_eqOn_of_inter_eq_of_eqOn — Mathlib

English

If e.IsImage s t and e' is another such with hs and Heq conditions, then EqOn of inverses on e.target ∩ t holds.

Русский

Если IsImage(e, s, t) и e' удовлетворяет условиям hs и Heq, то для обратных отображений на e.target ∩ t выполняется равенство по EqOn.

LaTeX

$$IsImage(e, s, t) \\Rightarrow ( (e'.IsImage s t) \\land (hs) \\land (Heq) ) \\Rightarrow EqOn(e^{-1}, e'^{-1}, e.target \\cap t)$$

Lean4

theorem symm_eqOn_of_inter_eq_of_eqOn {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t)
    (hs : e.source ∩ s = e'.source ∩ s) (Heq : EqOn e e' (e.source ∩ s)) : EqOn e.symm e'.symm (e.target ∩ t) :=
  h.toPartialEquiv.symm_eq_on_of_inter_eq_of_eqOn hs Heq

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