inf'_sup_distrib_right

Mathlib.Data.Finset.Lattice.Fold

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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