restr_toPartialEquiv' — Mathlib

English

If the source of an open partial homeomorphism e is contained in s, then restricting to s yields back e.

Русский

Если область определения e вложена в s, то ограничение до s восстанавливает e.

LaTeX

$$text{If } e.source \\subseteq s \\Rightarrow e.restr s = e$$

Lean4

theorem restr_toPartialEquiv' (s : Set X) (hs : IsOpen s) : (e.restr s).toPartialEquiv = e.toPartialEquiv.restr s := by
  rw [e.restr_toPartialEquiv, hs.interior_eq]

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