inf_union

Mathlib.Data.Finset.Lattice.Fold

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

English

The infimum over the union is the infimum of the two infima: (s1 ∪ s2).inf f = s1.inf f ⊓ s2.inf f.

Русский

Infimum над объединением равен meet'у инфимумов: (s1 ∪ s2).inf f = s1.inf f ⊓ s2.inf f.

LaTeX

$$$ (s_1 \cup s_2).inf f = s_1.inf f \wedge s_2.inf f $$$

Lean4

theorem inf_union [DecidableEq β] : (s₁ ∪ s₂).inf f = s₁.inf f ⊓ s₂.inf f :=
  eq_of_forall_le_iff fun c ↦ by simp [or_imp, forall_and]

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

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

Разделы

Аффилиация

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