comp_ite — Mathlib

English

The composition with a conditional commutes with the conditional: (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'.

Русский

Композиция с условием согласуется с условной конструкцией: (f ≫ если P тогда g иначе g') = если P тогда f ≫ g иначе f ≫ g'.

LaTeX

$$$ {P:\\text{Prop}} [\\Decidable P] {X Y Z} (f:X\\to Y) (g,g':Y\\to Z): (f \\gg \\, \\text{ite}(P\\,g\\,g')) = \\text{ite}(P\\, (f\\gg g)\\,(f\\gg g')) $$$

Lean4

theorem comp_ite {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z) :
    (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g' := by aesop

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