castLE_injective

Mathlib.Data.Fin.SuccPred

URI: https://scilib.ai/kg/mathlib#Fin.castLE_injective

English

If m ≤ n, Fin.castLE hmn is injective.

Русский

Если m ≤ n, Fin.castLE hmn инъективен.

LaTeX

$$$\\forall {m \\le n},\\; \\mathrm{Injective}(\\mathrm{Fin.castLE} hmn)$$$

Lean4

theorem castLE_injective (hmn : m ≤ n) : Injective (castLE hmn) := fun _ _ hab ↦ Fin.ext (congr_arg val hab :)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru