finsetImage_castAdd_Ioc — Mathlib

English

For any Fin n and m, the image of the half-open interval Ioc i j under castAdd m is Ioc (castAdd m i) (castAdd m j).

Русский

Для любых i, j ∈ Fin n и m ∈ ℕ образ Ioc i j под castAdd m равен Ioc (castAdd m i) (castAdd m j).

LaTeX

$$$ (\mathrm{Finset}.Ioc\, i\, j).image (\mathrm{Fin.castAdd}\, m) = \mathrm{Finset}.Ioc\ (\mathrm{Fin.castAdd}\, m\, i)\ (\mathrm{Fin.castAdd}\, m\, j) $$$

Lean4

@[simp]
theorem finsetImage_castAdd_Ioc (m) (i j : Fin n) : (Ioc i j).image (castAdd m) = Ioc (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_Ioc ..

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