map_mul_zero_of_map_zero — Mathlib

English

Under the assumptions, we have 0 ≤ c f x for all x.

Русский

При данных предположениях для каждого x выполняется 0 ≤ c f(x).

LaTeX

$$$0 \le c \cdot f(x)$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then given `x y : R` with
  `f x = 0`, we have `f (x * y) = 0`. -/
theorem map_mul_zero_of_map_zero (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) {x : R}
    (hx : f x = 0) (y : R) : f (x * y) = 0 :=
  by
  replace f_mul : f (x * y) ≤ 0 := by simpa [hx] using f_mul x y
  exact le_antisymm f_mul (f_nonneg _)

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