inf_sup_distrib_right

Mathlib.Data.Finset.Lattice.Fold

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

English

Infimum distributes over Finset infimum from the right: s.inf f ⊓ a = s.inf (f i ⊓ a).

Русский

Inf распределяется над инфомумом справа: s.inf f ⊓ a = s.inf (f i ⊓ a).

LaTeX

$$$ s.\\inf f \\wedge a = s.\\inf (\\lambda i, f i \\wedge a) $$$

Lean4

theorem inf_sup_distrib_right (s : Finset ι) (f : ι → α) (a : α) : s.inf f ⊔ a = s.inf fun i => f i ⊔ a :=
  @sup_inf_distrib_right αᵒᵈ _ _ _ _ _ _

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

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

Разделы

Аффилиация

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