le_max_iff_min_le — Mathlib

English

For natural numbers a,b,c, we have -c ≤ max(-a,-b) iff min(a,b) ≤ c.

Русский

Для натуральных a,b,c выполняется -c ≤ max(-a,-b) тогда и только тогда, когда min(a,b) ≤ c.

LaTeX

$$-c \le \max(-a,-b) \iff \min(a,b) \le c$$

Lean4

theorem le_max_iff_min_le {a b c : ℕ} :
    Multiplicative.ofAdd (-c : ℤ) ≤ max (Multiplicative.ofAdd (-a : ℤ)) (Multiplicative.ofAdd (-b : ℤ)) ↔ min a b ≤ c :=
  by rw [le_max_iff, ofAdd_le, ofAdd_le, neg_le_neg_iff, neg_le_neg_iff, Int.ofNat_le, Int.ofNat_le, ← min_le_iff]

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