sups_eq_self

Mathlib.Data.Set.Sups

URI: https://scilib.ai/kg/mathlib#Set.sups_eq_self

English

Equality s ⊻ s = s holds exactly when s is SupClosed.

Русский

Равенство s ⊻ s = s реализуется тогда, когда s замкнуто по верхнему пределу.

LaTeX

$$$ s \\veebar s = s \\iff \\operatorname{SupClosed}(s) $$$

Lean4

@[simp]
theorem sups_eq_self : s ⊻ s = s ↔ SupClosed s :=
  subset_sups_self.le.ge_iff_eq'.symm.trans sups_subset_self

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

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

Разделы

Аффилиация

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