eraseLead_ne_zero — Mathlib

English

If the support of f has at least two elements, then eraseLead f is nonzero.

Русский

Если поддержка f содержит не менее двух элементов, то eraseLead f не равно нулю.

LaTeX

$$eraseLead(f) ≠ 0 whenever #f.support ≥ 2$$

Lean4

theorem eraseLead_ne_zero (f0 : 2 ≤ #f.support) : eraseLead f ≠ 0 :=
  by
  rw [Ne, ← card_support_eq_zero, eraseLead_support]
  exact (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

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