mul_sup — Mathlib

English

Multiplication distributes over the binary supremum: a · (b ⊔ c) = (a · b) ⊔ (a · c) for a,b,c ∈ ℝ≥0.

Русский

Умножение распределяется по верхнему пределу: a · (b ⊔ c) = (a · b) ⊔ (a · c) для a,b,c ∈ ℝ≥0.

LaTeX

$$$ a * (b \\lor c) = a * b \\lor a * c, \\quad a,b,c \\in \\mathbb{R}_{\\ge 0}. $$$

Lean4

theorem mul_sup (a b c : ℝ≥0) : a * (b ⊔ c) = a * b ⊔ a * c :=
  mul_max_of_nonneg _ _ <| zero_le a

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