range_subset

Mathlib.Data.Finset.Range

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

English

range(n) is a subset of s if and only if every x < n is in s.

Русский

range(n) ⊆ s тогда и только тогда, когда каждый x < n принадлежит s.

LaTeX

$$$$ \operatorname{range}(n) \subseteq s \;\iff\; \forall x, x < n \rightarrow x \in s. $$$$

Lean4

@[grind =]
theorem range_subset {n s} : range n ⊆ s ↔ ∀ x, x < n → x ∈ s := by grind

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

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

Разделы

Аффилиация

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