sups_eq_self

Mathlib.Data.Finset.Sups

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

English

The self-image of sups preserves equality up to propext equivalence: Eq (sups s s) s = SupClosed(s).

Русский

Сохранение равенства при образе супов через прообраз: Eq (sups s s) s = SupClosed(s).

LaTeX

$$$\mathrm{Eq}(\mathrm{hasSups}.sups\; s\; s, \mathrm{supClosed}(s))$$$

Lean4

@[simp]
theorem sups_eq_self : s ⊻ s = s ↔ SupClosed (s : Set α) := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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