filter_le_eq_Ici

Mathlib.Order.Interval.Finset.Basic

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

English

In a finite type, the set {x | a ≤ x} equals Ici(a).

Русский

В конечном типе множество {x | a ≤ x} равно Ici(a).

LaTeX

$$$\{x \in \alpha \mid a \le x\} = \mathrm{Ici}(a)$$$

Lean4

theorem filter_le_eq_Ici [DecidablePred (a ≤ ·)] : ({x | a ≤ x} : Finset _) = Ici a := by ext; simp

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

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

Разделы

Аффилиация

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