min_mul_distrib — Mathlib

English

In a canonically ordered monoid, the meet with a distributes over multiplication: min(a, b c) = min(a, min(a,b) · min(a,c)).

Русский

В канонически упорядоченном моноиде операция meet распределяется над умножением: min(a, b c) = min(a, min(a,b) · min(a,c)).

LaTeX

$$\min(a, bc) = \min\big(a, \min(a,b) \cdot \min(a,c)\big)$$

Lean4

@[to_additive]
theorem min_mul_distrib (a b c : α) : min a (b * c) = min a (min a b * min a c) :=
  by
  rcases le_total a b with hb | hb
  · simp [hb, le_mul_right]
  · rcases le_total a c with hc | hc
    · simp [hc, le_mul_left]
    · simp [hb, hc]

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