map_one_ne_zero — Mathlib

English

If f is nonzero, nonnegative, and multiplicatively bounded, then f(1) ≠ 0.

Русский

Если f не тождественно ноль, неотрицательно и удовлетворяет ограничению по умножению, то f(1) ≠ 0.

LaTeX

$$$f(1) \neq 0$$$

Lean4

/-- If `f : R → ℝ` is a nonzero, nonnegative, multiplicatively bounded function, then `f 1 ≠ 0`. -/
theorem map_one_ne_zero (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    f 1 ≠ 0 := by
  intro h1
  specialize f_mul 1
  simp_rw [h1, one_mul, mul_zero, zero_mul] at f_mul
  obtain ⟨z, hz⟩ := Function.ne_iff.mp f_ne_zero
  exact hz <| (f_mul z).antisymm (f_nonneg z)

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