min_le_iff — Mathlib

English

For α a linear order, min(coe(a), coe(b)) ≤ coe(c) in WithZero α is equivalent to min(a,b) ≤ c in α.

Русский

Для линейного порядка α справедливо: min(coe(a), coe(b)) ≤ coe(c) в WithZero α эквивалентно min(a,b) ≤ c в α.

LaTeX

$$$\min(\mathrm{coe}(a), \mathrm{coe}(b)) \le \mathrm{coe}(c) \iff \min(a,b) \le c$$$

Lean4

protected theorem min_le_iff : min (a : WithZero α) b ≤ c ↔ min a b ≤ c := by
  simp only [WithZero.coe_le_coe, min_le_iff]

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