finsetImage_castLE_Iio — Mathlib

English

Let a ∈ Fin n and let h be a natural number embedding n into m with n ≤ m. Then the image of the lower interval Iio(a) under the order-embedding castLE h is exactly Iio of castLE h a, i.e., image(Iio(a)) = Iio(castLE h a).

Русский

Пусть a ∈ Fin n и пусть h задаёт вложение порядков через n ≤ m. Тогда образ нижнего промежутка Iio(a) под вложением castLE h равен Iio(castLE h a): image(Iio(a)) = Iio(castLE h a).

LaTeX

$$$\operatorname{image}(\operatorname{castLE}(h))(\mathrm{Iio}(a)) = \mathrm{Iio}(\operatorname{castLE}(h)\,a)$$$

Lean4

@[simp]
theorem finsetImage_castLE_Iio (h : n ≤ m) : (Iio a).image (castLE h) = Iio (castLE h a) := by simp [← coe_inj]

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