not_nonpos_iff_pos_of_sum_mem_range_root

English

Given a function f with sum in the root range and supported in b, not (f ≤ 0) is equivalent to 0 < f.

Русский

Для функции f с суммой в диапазоне корня и поддержкой внутри b, не (f ≤ 0) эквивалентно 0 < f.

LaTeX

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

Lean4

theorem not_nonpos_iff_pos_of_sum_mem_range_root (f : ι → ℤ) (hf : ∑ j ∈ b.support, f j • P.root j ∈ range P.root)
    (hf₀ : f.support ⊆ b.support) : (¬f ≤ 0) ↔ 0 < f :=
  by
  rw [Pi.lt_def]
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, ⟨i, hi⟩⟩ contra ↦ by simp [le_antisymm contra h] at hi⟩
  · rcases b.pos_or_neg_of_sum_smul_root_mem f hf hf₀ with h' | h'
    · exact le_of_lt h'
    · exfalso
      exact h (le_of_lt h')
  · contrapose! h; exact h

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