apply — Mathlib

English

The projection “apply” sends an affine equivalence to its underlying function; i.e., applying the simps projection yields the same map as the affine equivalence itself.

Русский

Проекция apply отображает аффинное эквивалентное отображение как обычную функцию; отображение совпадает с самим эквивалентом.

LaTeX

$$$ \mathrm{Simps.apply}(e) = e $$$

Lean4

/-- See Note [custom simps projection] -/
def apply (e : P₁ ≃ᵃ[k] P₂) : P₁ → P₂ :=
  e

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