mem_range_le

Mathlib.Data.Finset.Range

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

English

If x ∈ range(n) then x ≤ n.

Русский

Если x ∈ range(n), то x ≤ n.

LaTeX

$$$$ x \in \operatorname{range}(n) \Rightarrow x \le n. $$$$

Lean4

theorem mem_range_le {n x : ℕ} (hx : x ∈ range n) : x ≤ n := by grind

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

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

Разделы

Аффилиация

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