isRelUpperSet_self

Mathlib.Order.UpperLower.Relative

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

English

For any set s, IsRelUpperSet s (∈ s).

Русский

Для любого множества s верно IsRelUpperSet s (∈ s).

LaTeX

$$$IsRelUpperSet\\;s\\; (\\cdot \\in s)$$$

Lean4

@[simp]
theorem isRelUpperSet_self : IsRelUpperSet s (· ∈ s) := fun _ b ↦ ⟨b, fun _ _ ↦ id⟩

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

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

Разделы

Аффилиация

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