filter_ge_eq_Iic

Mathlib.Order.Interval.Finset.Basic

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

English

For a fixed a ∈ α, the Finset of all x with x ≤ a is exactly the initial interval Iic a.

Русский

Пусть дано a ∈ α. Тогда Finset всех x с x ≤ a совпадает с Iic a.

LaTeX

$$$\bigl\{ x \in \alpha : x \le a \bigr\} = \mathrm{Iic}(a).$$$

Lean4

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

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

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

Разделы

Аффилиация

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