zero_smul_nonneg — Mathlib

English

If g is nonempty (NeBot), then 0 ≤ (0) • g; i.e., the zero on α smul g is nonnegative in the filter order.

Русский

Если g ненулевой, то 0 ≤ 0 • g; т.е. нуль слева при умножении на g неотрицателен в порядке фильтров.

LaTeX

$$$g \\text{ is nonempty} \\implies 0 \\le 0_{\\alpha} \\cdot g$$$

Lean4

theorem zero_smul_nonneg (hg : g.NeBot) : 0 ≤ (0 : Filter α) • g :=
  le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, hb⟩ := hg.nonempty_of_mem h₂
    ⟨_, h₁, _, hb, zero_smul _ _⟩

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