seminormFromBounded_ker — Mathlib

English

If f is nonnegative and multiplicatively bounded, the kernel (zero-set) of seminormFromBounded' f equals the kernel of f.

Русский

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

LaTeX

$$$(0 \le f) \land (\forall x,y,\ f(xy) \le c f(x) f(y))\Rightarrow (\operatorname{ker}(\operatorname{seminormFromBounded'} f) = \operatorname{ker}(f))$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then the kernel of
  `seminormFromBounded' f` equals the kernel of `f`. -/
theorem seminormFromBounded_ker (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0} := by
  ext x
  exact seminormFromBounded_eq_zero_iff f_nonneg f_mul x

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