le_max_iff — Mathlib

English

For a linear order α, and a,b,c ∈ α, a ≤ max(b,c) in WithZero α if and only if a ≤ max(b,c) in α.

Русский

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

LaTeX

$$$\forall a,b,c \in \alpha:\; a \le \max(b,c) \text{ в } \mathrm{WithZero}\,\alpha \iff a \le \max(b,c) \text{ в } \alpha$$$

Lean4

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

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