lcongr_symm_single — Mathlib

English

The inverse of lcongr, on a singleton, corresponds to taking the symmetrically inverse singleton in the index and codomain.

Русский

Обратное отображение lcongr на единичном элементе соответствует соответствующему симметрически обратному элементу индекса и кода.

LaTeX

$$$(lcongr\,e_1\,e_2)^{-1}\;(\mathrm{single}\;k\;n) = \mathrm{single}\;(e_1^{-1}(k))\,(e_2^{-1}(n))$$$

Lean4

theorem lcongr_symm_single {ι κ : Sort _} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (k : κ) (n : N) :
    (lcongr e₁ e₂).symm (Finsupp.single k n) = Finsupp.single (e₁.symm k) (e₂.symm n) :=
  by
  apply_fun (lcongr e₁ e₂ : (ι →₀ M) → (κ →₀ N)) using (lcongr e₁ e₂).injective
  simp

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