seminormFromBounded_eq_zero_iff — Mathlib

English

seminormFromBounded' f x = 0 iff f x = 0.

Русский

seminormFromBounded' f x = 0 тогда и только тогда, когда f x = 0.

LaTeX

$$$\operatorname{seminormFromBounded}' f x = 0 \iff f x = 0$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
  `seminormFromBounded' f x = 0` if and only if `f x = 0`. -/
theorem seminormFromBounded_eq_zero_iff (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
    seminormFromBounded' f x = 0 ↔ f x = 0 :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have hf := seminormFromBounded_ge f_nonneg f_mul x
    rw [h, mul_zero] at hf
    exact hf.antisymm (f_nonneg _)
  · have hf : seminormFromBounded' f x ≤ c * f x := seminormFromBounded_le f_nonneg f_mul x
    rw [h, mul_zero] at hf
    exact hf.antisymm (seminormFromBounded_nonneg f_nonneg f_mul x)

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