not_nonneg_iff_neg_of_sum_mem_range_root

English

Similar to Not Nonpositive, the negation of nonnegativity of f is equivalent to f < 0 under the same hypotheses.

Русский

Аналогично, отрицание неотрицательности f эквивалентно f < 0 при тех же предположениях.

LaTeX

$$(¬0 ≤ f) ↔ f < 0$$

Lean4

theorem not_nonneg_iff_neg_of_sum_mem_range_root (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ range P.root)
    (hf₀ : f.support ⊆ b.support) : (¬0 ≤ f) ↔ f < 0 :=
  by
  replace hf : ∑ j ∈ b.support, (-f) j • P.root j ∈ range P.root := by rw [← neg_mem_range_root_iff]; simpa
  have := b.not_nonpos_iff_pos_of_sum_mem_range_root (-f) hf (by simpa)
  simp_all

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