restr_of_source_subset — Mathlib

English

If A contains f.source, then restricting to A yields the same equidecomposition: f.restr A = f.

Русский

Если A содержит f.source, то ограничение до A сохраняет эквидекомпозицию: f.restr A = f.

LaTeX

$$$\forall f:\mathrm{Equidecomp}(X,G), \forall A, f.source \subseteq A \Rightarrow f.restr A = f.$$$

Lean4

theorem restr_of_source_subset {f : Equidecomp X G} {A : Set X} (hA : f.source ⊆ A) : f.restr A = f :=
  by
  apply toPartialEquiv_injective
  rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]

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