mul — Mathlib

English

If f,g: X → Y are locally constant and Y has a multiplication, then the product f · g is locally constant.

Русский

Если f,g: X → Y локально константны и Y имеет умножение, то произведение f · g локально константно.

LaTeX

$$IsLocallyConstant f × g$$

Lean4

@[to_additive]
theorem mul [Mul Y] ⦃f g : X → Y⦄ (hf : IsLocallyConstant f) (hg : IsLocallyConstant g) : IsLocallyConstant (f * g) :=
  hf.comp₂ hg (· * ·)

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