subset_sups_self

Mathlib.Data.Finset.Sups

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

English

The inclusion s ⊻ s ⊆ s is equivalent to SupClosed (as a set).

Русский

Включение s ⊻ s ⊆ s эквивалентно SupClosed для множества s.

LaTeX

$$$ (s \oplus s) \subseteq s \;\iff\; \mathrm{SupClosed}(s) $$$

Lean4

theorem subset_sups_self : s ⊆ s ⊻ s := fun _a ha ↦ mem_sups.2 ⟨_, ha, _, ha, sup_idem _⟩

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

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

Разделы

Аффилиация

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