sup'_id_eq_csSup

Mathlib.Order.ConditionallyCompleteLattice.Finset

URI: https://scilib.ai/kg/mathlib#Finset.sup'_id_eq_csSup

English

The supremum of a finite set with the identity function equals the supremum of the set itself.

Русский

Супремум множества с функцией идентичности равен супремусу самого множества.

LaTeX

$$$s.sup' H id = sSup s$$$

Lean4

theorem sup'_id_eq_csSup (s : Finset α) (hs) : s.sup' hs id = sSup s := by rw [sup'_eq_csSup_image s hs, Set.image_id]

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

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

Разделы

Аффилиация

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