map_pow_ne_zero — Mathlib

English

If f is nonzero at x and x is a unit, then f(x^n) ≠ 0 for all n ∈ ℕ.

Русский

Если f(x) ≠ 0 и x является единицей, то f(x^n) ≠ 0 для всех n ∈ ℕ.

LaTeX

$$$f(x^n) \neq 0$ for all n ∈ \mathbb{N}$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative multiplicatively bounded function and `x : R` is a unit with
  `f x ≠ 0`, then for every `n : ℕ`, we have `f (x ^ n) ≠ 0`. -/
theorem map_pow_ne_zero (f_nonneg : 0 ≤ f) {x : R} (hx : IsUnit x) (hfx : f x ≠ 0) (n : ℕ)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) : f (x ^ n) ≠ 0 :=
  by
  have h1 : f 1 ≠ 0 := map_one_ne_zero (Function.ne_iff.mpr ⟨x, hfx⟩) f_nonneg f_mul
  intro hxn
  have : f 1 ≤ 0 := by simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)
  exact h1 <| this.antisymm (f_nonneg 1)

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