filter_lt_eq_Ioi

Mathlib.Order.Interval.Finset.Basic

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

English

In a finite type with a linear order, the Finset of elements with x > a coincides with Ioi(a).

Русский

В конечном типе с линейным порядком множество элементов, больше заданного a, совпадает с Ioi(a).

LaTeX

$$$\{x \in \alpha \mid a < x\} = \mathrm{Ioi}(a)$$$

Lean4

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

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

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

Разделы

Аффилиация

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