restr_source' — Mathlib

English

A variation of restr_toPartialEquiv with a minor interior adjustment yields equality of the restricted partial equivalences.

Русский

Вариация restr_toPartialEquiv с малым изменением внутренности приводит к равенству ограниченных частичных эквивалентностей.

LaTeX

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

Lean4

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

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