equivCongrLeft_apply — Mathlib

English

For h : ι ≃ κ, f ∈ ⨁ i, β i and k ∈ κ, (equivCongrLeft h) f k = f (h.symm k).

Русский

Для h: ι ≃ κ, f ∈ ∑ β i и k ∈ κ, (equivCongrLeft h) f k = f (h.symm k).

LaTeX

$$equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : equivCongrLeft h f k = f (h.symm k)$$

Lean4

@[simp]
theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : equivCongrLeft h f k = f (h.symm k) := by
  exact DFinsupp.comapDomain'_apply _ h.right_inv _ _

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