isLUB_sup

Mathlib.Data.Finset.Lattice.Fold

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

English

The image f''s together with the supremum s.sup f satisfies IsLUB: (f''s, s.sup f).

Русский

Изображение f''s и верхняя грань s.sup f образуют свойство наименьшей верхней грани.

LaTeX

$$$ IsLUB (f'' s) (s.sup f) $$$

Lean4

theorem isLUB_sup : IsLUB (f '' s) (s.sup f) := by simp +contextual [IsLUB, IsLeast, upperBounds, lowerBounds, le_sup]

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

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

Разделы

Аффилиация

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