strictMono_castLE

Mathlib.Order.Fin.Basic

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

English

For all m,n with n ≤ m, the castLE h : Fin n → Fin m is strictly monotone.

Русский

Для всех m, n с n ≤ m отображение castLE h: Fin n → Fin m строго монотонно.

LaTeX

$$$\forall m\ n : \mathbb{N},\ (n \le m) \Rightarrow \mathrm{StrictMono}(\mathrm{castLE}\ h)$$$

Lean4

theorem strictMono_castLE (h : n ≤ m) : StrictMono (castLE h : Fin n → Fin m) := fun _ _ ↦ id

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

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

Разделы

Аффилиация

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