map_castLEEmb_Ico — Mathlib

English

Let a,b ∈ Fin n and h with n ≤ m. Then the image under castLEEmb h of the open-closed interval Ico(a,b) is the interval Ico between castLE h a and castLE h b: map(Ico(a,b)) = Ico(castLE h a, castLE h b).

Русский

Пусть a,b ∈ Fin n и h с n ≤ m. Тогда образ Ico(a,b) под castLEEmb h равен Ico(castLE h a, castLE h b).

LaTeX

$$$\operatorname{Finset.map}(\operatorname{castLEEmb}(h))(\mathrm{Ico}(a,b)) = \mathrm{Ico}(\operatorname{castLE}(h)a, \operatorname{castLE}(h)b)$$$

Lean4

@[simp]
theorem map_castLEEmb_Ico (h : n ≤ m) : (Ico a b).map (castLEEmb h) = Ico (castLE h a) (castLE h b) := by
  simp [← coe_inj]

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