English
Equivalence between dfinsupps induced by a left-equivalence h: ι ≃ κ, i.e., (Π₀ i, β i) ≃ Π₀ k, β (h.symm k).
Русский
Эквивалентность dfinsupp, получаемая из левого эквивайленса h: ι ≃ κ, то есть (Π₀ i, β i) ≃ Π₀ k, β (h.symm k).
LaTeX
$$$(\\Pi_0 i, \\beta i) \\cong (\\Pi_0 k, \\, \\beta (h^{-1}(k)))$$$
Lean4
/-- Reindexing terms of a dfinsupp.
This is the dfinsupp version of `Equiv.piCongrLeft'`. -/
@[simps apply]
def equivCongrLeft [∀ i, Zero (β i)] (h : ι ≃ κ) : (Π₀ i, β i) ≃ Π₀ k, β (h.symm k)
where
toFun := comapDomain' h.symm h.right_inv
invFun
f :=
mapRange (fun i => Equiv.cast <| congr_arg β <| h.symm_apply_apply i)
(fun i => (Equiv.cast_eq_iff_heq _).mpr <| by rw [Equiv.symm_apply_apply])
(@comapDomain' _ _ _ _ h _ h.left_inv f)
left_inv
f := by
ext i
rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq, h.symm_apply_apply]
right_inv
f := by
ext k
rw [comapDomain'_apply, mapRange_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq, h.apply_symm_apply]
