image_castLE_Iic — Mathlib

English

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

Русский

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

LaTeX

$$$castLE(h) '' Iic i = Iic (castLE(h) i)$$$

Lean4

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

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