map_app — Mathlib

English

The map-app property of an isometry equivalence: applying to an element gives the same evaluation as applying to the corresponding argument.

Русский

Свойство отображения применимо к изометрическому эквиваленту: применение к элементу даёт такое же значение, как и применение к соответствующему аргументу.

LaTeX

$$$\forall m, Q_2 (f(m)) = Q_1(m)$$$

Lean4

@[simp]
theorem map_app (f : Q₁.IsometryEquiv Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
  f.map_app' m

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