source_restr — Mathlib

English

If A is contained in f.source, then restricting f to A yields a new equidecomposition with source A.

Русский

Если A ⊆ f.source, то ограничение f до A даёт эквидекомпозицию с источником A.

LaTeX

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

Lean4

theorem source_restr (f : Equidecomp X G) {A : Set X} (hA : A ⊆ f.source) : (f.restr A).source = A := by
  rw [restr_source, inter_eq_self_of_subset_right hA]

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