preimage_castLE_Ioc_castLE — Mathlib

English

Let i, j ∈ Fin(m) and h with m ≤ n. Then the preimage of the open-closed interval Ioc at castLE(h i) to castLE(h j) under castLE(h) equals Ioc(i, j).

Русский

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

LaTeX

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

Lean4

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

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