card_support_le_one_of_eraseLead_eq_zero

English

If eraseLead(f) = 0, then the support of f has size at most 1.

Русский

Если eraseLead(f) = 0, то опора f имеет размер не более 1.

LaTeX

$$$\operatorname{eraseLead}(f) = 0 \Rightarrow |\operatorname{Supp}(f)| \le 1$$$

Lean4

theorem card_support_le_one_of_eraseLead_eq_zero (h : f.eraseLead = 0) : #f.support ≤ 1 :=
  by
  by_cases hpz : f = 0
  case pos => simp [hpz]
  case neg => exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

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