add_comp' — Mathlib

English

The same as add_comp but expressed with the underlying functions; (κ + η) map form equals sum of maps.

Русский

То же самое, что и add_comp, но выражено через отображения; сумма отображений эквивалентна композиции.

LaTeX

$$$(\\hat{\\kappa} + \\hat{\\eta}) \\circ_{m} \\mu = \\hat{\\kappa} \\circ_{m} \\mu + \\hat{\\eta} \\circ_{m} \\mu$$$

Lean4

/-- Same as `add_comp` except that it uses `⇑κ + ⇑η` instead of `⇑(κ + η)` in order to have
a simp-normal form on the left of the equality. -/
@[simp]
theorem add_comp' : (⇑κ + ⇑η) ∘ₘ μ = κ ∘ₘ μ + η ∘ₘ μ := by rw [← Kernel.coe_add, add_comp]

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