infs_self_subset

Mathlib.Data.Finset.Sups

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

English

s ⊼ s ⊆ s if and only if s is Inf-Closed as a subset of α.

Русский

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

LaTeX

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

Lean4

theorem infs_self_subset : s ⊼ s ⊆ s ↔ InfClosed (s : Set α) :=
  infs_subset_iff

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

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

Разделы

Аффилиация

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