preimage_addNat_Iic_addNat — Mathlib

English

For all m ∈ ℕ and i ∈ Fin(n), the preimage of Iic(i.addNat m) under x ↦ x + m is Iic i.

Русский

Для всех m ∈ ℕ и i ∈ Fin(n) предобраз подстановки x ↦ x + m для Iic(i.addNat m) равен Iic i.

LaTeX

$$$$ \\mathrm{Set.preimage}(\\\\mathrm{Fin.natAdd}(m))(\\\\mathrm{Set.Iic}(i)) = \\\\mathrm{Set.Iic}(i). $$$$

Lean4

@[simp]
theorem preimage_addNat_Iic_addNat (m) (i : Fin n) : (addNat · m) ⁻¹' Iic (i.addNat m) = Iic i := by ext; simp

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