dite_tensor

Mathlib.CategoryTheory.Monoidal.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.dite_tensor

Lean4

theorem dite_tensor {P : Prop} [Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) :
    (if h : P then g h else g' h) ⊗ₘ f = if h : P then g h ⊗ₘ f else g' h ⊗ₘ f := by split_ifs <;> rfl

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

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

Разделы

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

Аффилиация

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