English
Let P be a Prop and X,Y,Z objects with f:X→Y and g:P → (Y→Z), g':¬P → (Y→Z). Then f ≫ if h:P then g h else g' h equals if h:P then f ≫ g h else f ≫ g' h.
Русский
Пусть P — пропозиция и существуют функции g:P → (Y→Z) и g':¬P → (Y→Z). Тогда f ∘ (если P тогда g(h) иначе g'(h)) = (если P тогда f ∘ g(h) иначе f ∘ g'(h)).
LaTeX
$$$ {P:\\text{Prop}} [\\Decidable P] {X Y Z} (f:X\\to Y) (g:P\\to(Y\\to Z)) (g':\\neg P\\to(Y\\to Z)) : (f \\gg \\text{if } h:\\!P \\text{ then } g\\,h \\text{ else } g'\\,h) = \\text{if } h:\\!P \\text{ then } f\\gg (g\\,h) \\text{ else } f\\gg (g'\\,h) $$$
Lean4
theorem comp_dite {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (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 aesop
