mem

Mathlib.Data.List.Intervals

URI: https://scilib.ai/kg/mathlib#List.Ico.mem

English

An element l belongs to Ico n m iff n ≤ l < m.

Русский

Элемент l принадлежит Ico n m тогда и только тогда, когда n ≤ l < m.

LaTeX

$$$l \in \operatorname{Ico}(n,m) \iff n \le l \land l < m$$$

Lean4

@[simp]
theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m :=
  by
  suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
  cutsat

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

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

Разделы

Аффилиация

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