inf'_sup_distrib_left

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.inf'_sup_distrib_left

English

In a distributive lattice, a ⊔ s.inf' hs f = s.inf' hs (a ⊔ f i).

Русский

В распределительной решётке a ⊔ (inf' s f) = inf' s (a ⊔ f).

LaTeX

$$$a \sqcup s.inf' hs f = s.inf' hs (a \sqcup f).$$$

Lean4

theorem inf'_sup_distrib_left (f : ι → α) (a : α) : a ⊔ s.inf' hs f = s.inf' hs fun i => a ⊔ f i :=
  @sup'_inf_distrib_left αᵒᵈ _ _ _ hs _ _

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

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

Разделы

Аффилиация

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