iSup_min

Mathlib.CategoryTheory.Subpresheaf.Basic

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

English

The infimum with a fixed subpresheaf T distributes over a supremum: (⨆ i, S_i) ⊓ T = ⨆ i, S_i ⊓ T.

Русский

infimum над sup распределяется через infimum: (⨆ i, S_i) ⊓ T = ⨆ i, S_i ⊓ T.

LaTeX

$$$\\left( \\bigvee_i S_i \\right) \\wedge T = \\bigvee_i (S_i \\wedge T)$$$

Lean4

theorem iSup_min {ι : Type*} (S : ι → Subpresheaf F) (T : Subpresheaf F) : (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T := by aesop

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

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

Разделы

Аффилиация

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