filter_gt_eq_Iio

Mathlib.Order.Interval.Finset.Basic

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

English

For a fixed element a in α, the Finset of all x with x < a is exactly the initial segment Iio a.

Русский

Пусть дано a ∈ α. Тогда множество Finset всех x с x < a совпадает с Iio a.

LaTeX

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

Lean4

theorem filter_gt_eq_Iio [DecidablePred (· < a)] : ({x | x < a} : Finset _) = Iio a := by ext; simp

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

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

Разделы

Аффилиация

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