map_target — Mathlib

English

If x lies in the target of an equidecomposition, then its symmetric image lies in the source.

Русский

Если x принадлежит целевой части эквидекомпозиции, то ее симметричная проекция лежит в исходной части.

LaTeX

$$$x \\in f\\text{.target} \\Rightarrow f^{\\mathrm{symm}}(x) \\in f^{\\mathrm{source}}.$$$

Lean4

theorem map_target {f : Equidecomp X G} {x : X} (h : x ∈ f.target) : f.symm x ∈ f.source :=
  f.toPartialEquiv.map_target h

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