image_castLE_uIcc — Mathlib

English

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

Русский

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

LaTeX

$$$castLE(h) '' uIcc (castLE(h i)) (castLE(h j)) = uIcc(i, j)$$$

Lean4

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

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