add_le — Mathlib

English

For any d1, d2, d3 in the ManyOneDegree order, d1 + d2 ≤ d3 if and only if d1 ≤ d3 and d2 ≤ d3.

Русский

Для любых степеней d1, d2, d3 в порядке ManyOneDegree, выполняется: d1 + d2 ≤ d3 тогда и только тогда, когда d1 ≤ d3 и d2 ≤ d3.

LaTeX

$$$$ d_1 + d_2 \\le d_3 \\iff d_1 \\le d_3 \\land d_2 \\le d_3. $$$$

Lean4

@[simp]
protected theorem add_le {d₁ d₂ d₃ : ManyOneDegree} : d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃ :=
  by
  induction d₁ using ManyOneDegree.ind_on
  induction d₂ using ManyOneDegree.ind_on
  induction d₃ using ManyOneDegree.ind_on
  simpa only [← add_of, of_le_of] using disjoin_le

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