map_dite — Mathlib

English

Let F : C ⥤ D, D a category, and P a Prop with Decidable P. For f : P → (X ⟶ Y) and g : ¬P → (X ⟶ Y), F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h).

Русский

Пусть F : C ⥤ D; P — произвольное предикатное условие с разрешимостью. Тогда отображение F.map применимо к выражению с разбиением по P: F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h).

LaTeX

$$$ F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h). $$$

Lean4

@[simp]
theorem map_dite (F : C ⥤ D) {X Y : C} {P : Prop} [Decidable P] (f : P → (X ⟶ Y)) (g : ¬P → (X ⟶ Y)) :
    F.map (if h : P then f h else g h) = if h : P then F.map (f h) else F.map (g h) := by cat_disch

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