max_min

Mathlib.CategoryTheory.Subpresheaf.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.max_min

English

Distributivity holds between maximum and minimum: (S1 ⊔ S2) ⊓ T equals (S1 ⊓ T) ⊔ (S2 ⊓ T).

Русский

Распределимость между максимумом и минимумом: (S1 ⊔ S2) ⊓ T = (S1 ⊓ T) ⊔ (S2 ⊓ T).

LaTeX

$$$(S_1 \\uplus S_2) \\sqcap T = (S_1 \\sqcap T) \\uplus (S_2 \\sqcap T)$$$

Lean4

theorem max_min (S₁ S₂ T : Subpresheaf F) : (S₁ ⊔ S₂) ⊓ T = (S₁ ⊓ T) ⊔ (S₂ ⊓ T) := by aesop

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

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

Разделы

Аффилиация

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