range_mono

Mathlib.Data.Finset.Range

URI: https://scilib.ai/kg/mathlib#Finset.range_mono

English

The function n ↦ range(n) is monotone with respect to inclusion: if n ≤ m then range(n) ⊆ range(m).

Русский

Функция n ↦ range(n) монотонна по включению: если n ≤ m, то range(n) ⊆ range(m).

LaTeX

$$$$ \text{range is monotone: }\forall n,m,\; n \le m \Rightarrow \operatorname{range}(n) \subseteq \operatorname{range}(m). $$$$

Lean4

theorem range_mono : Monotone range := fun _ _ => range_subset_range.2

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

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

Разделы

Аффилиация

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