Ico_filter_lt_of_le_left

Mathlib.Order.Interval.Finset.Basic

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

← MathLib Explorer

English

If c ≤ a, then the subset {x ∈ Ico(a, b) | x < c} is empty.

Русский

Если c ≤ a, то {x ∈ Ico(a,b) | x < c} = ∅.

LaTeX

$$$ c \le a \Rightarrow \{x \in Ico(a,b) \mid x < c\} = \emptyset $$$

Lean4

theorem Ico_filter_lt_of_le_left [DecidablePred (· < c)] (hca : c ≤ a) : {x ∈ Ico a b | x < c} = ∅ :=
  filter_false_of_mem fun _ hx => (hca.trans (mem_Ico.1 hx).1).not_gt

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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