sup'_inf_distrib_right

Mathlib.Data.Finset.Lattice.Fold

URI: https://scilib.ai/kg/mathlib#Finset.sup'_inf_distrib_right

← MathLib Explorer

English

In a distributive lattice, s.sup' hs f ⊓ a = s.sup' hs (f i ⊓ a).

Русский

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

LaTeX

$$$s.sup' hs f \sqcap a = s.sup' hs (f \cdot \sqcap a).$$$

Lean4

theorem sup'_inf_distrib_right (f : ι → α) (a : α) : s.sup' hs f ⊓ a = s.sup' hs fun i => f i ⊓ a := by
  rw [inf_comm, sup'_inf_distrib_left]; simp_rw [inf_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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