mem_pregroupoid_of_eqOnSource — Mathlib

English

If two open partial homeomorphisms e and e' are equivalent and e has the PG property on its source, then e' also has the PG property on its source.

Русский

Если две открытые частичные гомоморфизмы e и e' эквивалентны и e обладает свойством PG на своем источнике, то и e' обладает свойством PG на своем источнике.

LaTeX

$$$(e \\approx e') \\to (PG.property\\; e\\; e.source \\to PG.property\\; e'\\; e'.source)$$

Lean4

theorem mem_pregroupoid_of_eqOnSource (PG : Pregroupoid H) {e e' : OpenPartialHomeomorph H H} (he' : e ≈ e')
    (he : PG.property e e.source) : PG.property e' e'.source :=
  by
  rw [← he'.1]
  exact PG.congr e.open_source he'.eqOn.symm he

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