inf_inf

Mathlib.Data.Finset.Lattice.Fold

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

English

The infimum of the pointwise infimum equals the infimum of the pointwise infima: inf f ⊓ g = inf f ⊓ inf g.

Русский

Infimum по точечному и-подобному равен инфимума f и g: s.inf (f ⊓ g) = s.inf f ⊓ s.inf g.

LaTeX

$$$ s.inf (f \inf g) = s.inf f \inf s.inf g $$$

Lean4

theorem inf_inf : s.inf (f ⊓ g) = s.inf f ⊓ s.inf g :=
  @sup_sup αᵒᵈ _ _ _ _ _ _

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

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

Разделы

Аффилиация

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