range_subset_range

Mathlib.Data.Finset.Range

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

English

range(n) is contained in range(m) precisely when n ≤ m.

Русский

range(n) ⊆ range(m) тогда и только тогда, когда n ≤ m.

LaTeX

$$$$ \operatorname{range}(n) \subseteq \operatorname{range}(m) \;\iff\; n \le m. $$$$

Lean4

@[simp]
theorem range_subset_range {n m} : range n ⊆ range m ↔ n ≤ m := by grind

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

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

Разделы

Аффилиация

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