restr — Mathlib

English

Restriction of equivalent open partial homeomorphisms to the same set remains equivalent: if e ≈ e' then e.restr s ≈ e'.restr s.

Русский

Ограничения эквивалентных гомеоморфизмов на одно и то же множество сохраняют эквивалентность: e ≈ e' ⇒ e.restr s ≈ e'.restr s.

LaTeX

$$$ (e \approx e') \Rightarrow e.restr s \approx e'.restr s $$$

Lean4

/-- Restriction of open partial homeomorphisms respects equivalence -/
theorem restr {e e' : OpenPartialHomeomorph X Y} (he : e ≈ e') (s : Set X) : e.restr s ≈ e'.restr s :=
  PartialEquiv.EqOnSource.restr he _

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