apply — Mathlib

English

The Simps.apply projection simply returns the given equivalence h itself as a map.

Русский

Проекция Simps.apply просто возвращает данное эквивалентное отображение h как карту.

LaTeX

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

Lean4

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def apply (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : Type*)
    [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) : E → E₂ :=
  h

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