restr_toPartialEquiv — Mathlib

English

Restricting the OpenPartialHomeomorph to an open subset induces a corresponding restriction on its underlying partial equivalence.

Русский

Ограничение OpenPartialHomeomorph до открытого подмножества порождает соответствующее ограничение на его базовую частичную эквивалентность.

LaTeX

$$$(e.restr s).toPartialEquiv = e.toPartialEquiv.restr (interior s)$$$

Lean4

@[simp, mfld_simps]
theorem restr_toPartialEquiv (s : Set X) : (e.restr s).toPartialEquiv = e.toPartialEquiv.restr (interior s) :=
  rfl

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