isUpperSet_univ

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#isUpperSet_univ

English

The universal set is an upper set: for all x, y with x ≤ y, if x ∈ univ then y ∈ univ.

Русский

Универсальное множество является верхним множеством: для любых x, y с x ≤ y, если x ∈ univ, то y ∈ univ.

LaTeX

$$$IsUpperSet(\mathrm{univ})$$$

Lean4

theorem isUpperSet_univ : IsUpperSet (univ : Set α) := fun _ _ _ => id

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

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

Разделы

Аффилиация

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