infs_self

Mathlib.Data.Finset.Sups

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

English

s ⊼ s = s if and only if s is Inf-Closed as a set.

Русский

s ⊼ s = s тогда и только если s является Inf-замкнутым множеством.

LaTeX

$$$ s \⊼ s = s \quad\Leftrightarrow\quad \operatorname{InfClosed} (s : \operatorname{Set} \alpha) $$$

Lean4

@[simp]
theorem infs_self : s ⊼ s = s ↔ InfClosed (s : Set α) := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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