preimage_natAdd_Icc_natAdd — Mathlib

English

For all m and i, j in Fin n, the preimage of Icc(natAdd m i) (natAdd m j) under natAdd m is Icc i j.

Русский

Для всех m и i, j ∈ Fin n, прообраз Icc(natAdd m i, natAdd m j) под natAdd m равен Icc i j.

LaTeX

$$$\operatorname{natAdd}(m)^{-1}(\mathrm{Icc}(\mathrm{natAdd}(m,i), \mathrm{natAdd}(m,j))) = \mathrm{Icc}(i, j)$$$

Lean4

@[simp]
theorem preimage_natAdd_Icc_natAdd (m) (i j : Fin n) : natAdd m ⁻¹' Icc (natAdd m i) (natAdd m j) = Icc i j := by ext;
  simp

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