tensor_dite

Mathlib.CategoryTheory.Monoidal.Category

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

Lean4

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

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

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

Разделы

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

Аффилиация

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