isGLB_inf

Mathlib.Data.Finset.Lattice.Fold

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

English

The image f''s and s.inf f form a greatest lower bound: IsGLB (f'' s) (s.inf f).

Русский

Образ f''s и inf f образуют наибольшую нижнюю грань: IsGLB (f'' s) (s.inf f).

LaTeX

$$$ IsGLB (f'' s) (s.inf f) $$$

Lean4

theorem isGLB_inf : IsGLB (f '' s) (s.inf f) := by
  simp +contextual [IsGLB, IsGreatest, upperBounds, lowerBounds, inf_le]

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

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

Разделы

Аффилиация

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