val_strictMono

Mathlib.Order.Fin.Basic

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

English

The function val : Fin n → ℕ is strictly monotone.

Русский

Функция val: Fin n → ℕ строго монотонна.

LaTeX

$$$\mathrm{StrictMono}(\mathrm{val} : \mathrm{Fin}(n) \to \mathbb{N})$$$

Lean4

theorem val_strictMono : StrictMono (val : Fin n → ℕ) := fun _ _ ↦ id

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

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

Разделы

Аффилиация

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