seminormFromBounded_bddAbove_range

English

seminormFromBounded' f is a RingSeminorm on R.

Русский

seminormFromBounded' f — кольцевая семинормa на R.

LaTeX

$$$\text{seminormFromBounded}' f \text{ is a RingSeminorm on } R$$$

Lean4

/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then for every `x : R`,
  the image of `y ↦ f (x * y) / f y` is bounded above. -/
theorem seminormFromBounded_bddAbove_range (f_nonneg : 0 ≤ f) (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
    BddAbove (Set.range fun y ↦ f (x * y) / f y) := by
  use c * f x
  rintro r ⟨y, rfl⟩
  rcases (f_nonneg y).eq_or_lt' with hy0 | hy0
  · simpa [hy0] using seminormFromBounded_aux f_nonneg f_mul x
  · simpa [div_le_iff₀ hy0] using f_mul x y

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