preimage_castLE_Ioi_castLE — Mathlib

English

Let i ∈ Fin(m) and h with m ≤ n. Then the preimage of the open upper interval Ioi at castLE(h,i) under castLE(h) equals Ioi(i).

Русский

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

LaTeX

$$$castLE(h)^{-1}'\mathrm{Ioi}(\mathrm{castLE}(h,i)) = \mathrm{Ioi}(i)$$$

Lean4

@[simp]
theorem preimage_castLE_Ioi_castLE (i : Fin m) (h : m ≤ n) : castLE h ⁻¹' Ioi (castLE h i) = Ioi i :=
  rfl

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