smul_zero_nonneg — Mathlib

English

If f is nonempty (NeBot), then 0 ≤ f • 0 in the order of filters on β; i.e., smul of zero by a nontrivial filter is nonnegative.

Русский

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

LaTeX

$$$f \\text{ is nonempty} \\implies 0 \\le f \\cdot 0_{\\beta}$$$

Lean4

theorem smul_zero_nonneg (hf : f.NeBot) : 0 ≤ f • (0 : Filter β) :=
  le_smul_iff.2 fun _ h₁ _ h₂ =>
    let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
    ⟨_, ha, _, h₂, smul_zero _⟩

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