image_castLE_Icc — Mathlib

English

Let i, j ∈ Fin(m) and h with m ≤ n. Then the image of the closed interval Icc i j under castLE h equals Icc (castLE h i) (castLE h j).

Русский

Пусть i, j ∈ Fin(m) и h с m ≤ n. Тогда образ закрытого интервала Icc(i, j) под castLE(h) равен Icc(castLE(h)i, castLE(h)j).

LaTeX

$$$castLE(h) '' Icc i j = Icc (castLE(h) i) (castLE(h) j)$$$

Lean4

@[simp]
theorem image_castLE_Icc (i j : Fin m) (h : m ≤ n) : castLE h '' Icc i j = Icc (castLE h i) (castLE h j) :=
  val_injective.image_injective <| by simp [image_image]

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