English
For any φ and w, w ≤ lexOrder φ iff every d with toLex d < w has coeff d φ = 0.
Русский
Для любых φ и w выполняется: w ≤ lexOrder φ тогда и только тогда, когда для каждого d с toLex d < w коэффициент φ при d равен нулю.
LaTeX
$$$ w \le \operatorname{lexOrder}(\phi) \iff (\forall d,\; \text{toLex} d < w \Rightarrow \operatorname{coeff}(d,\phi) = 0)$$$
Lean4
theorem le_lexOrder_mul (φ ψ : MvPowerSeries σ R) : lexOrder φ + lexOrder ψ ≤ lexOrder (φ * ψ) :=
by
rw [le_lexOrder_iff]
intro d hd
rw [coeff_mul]
apply Finset.sum_eq_zero
rintro ⟨u, v⟩ h
simp only [Finset.mem_antidiagonal] at h
simp only
suffices toLex u < lexOrder φ ∨ toLex v < lexOrder ψ
by
rcases this with (hu | hv)
· rw [coeff_eq_zero_of_lt_lexOrder hu, zero_mul]
· rw [coeff_eq_zero_of_lt_lexOrder hv, mul_zero]
rw [or_iff_not_imp_left, not_lt, ← not_le]
intro hu hv
rw [← not_le] at hd
apply hd
simp only [← h, toLex_add, WithTop.coe_add, add_le_add hu hv]
