nonneg_prod_iff — Mathlib

English

The nonnegativity of the product equals the pairwise nonnegativity of its factors.

Русский

Непрерывность произведения равна по крайней мере неотрицательности его факторов по отдельности.

LaTeX

$$For all x: (Q1.prod Q2) x ≥ 0 iff (Q1 x ≥ 0) and (Q2 x ≥ 0)$$

Lean4

theorem nonneg_prod_iff [Preorder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} :
    (∀ x, 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ x, 0 ≤ Q₁ x) ∧ ∀ x, 0 ≤ Q₂ x :=
  by
  simp_rw [Prod.forall, prod_apply]
  constructor
  · intro h
    constructor
    · intro x; simpa only [add_zero, map_zero] using h x 0
    · intro x; simpa only [zero_add, map_zero] using h 0 x
  · rintro ⟨h₁, h₂⟩ x₁ x₂
    exact add_nonneg (h₁ x₁) (h₂ x₂)

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