continuous_of_le — Mathlib

English

If q is bounded by C times p on a shell, then q(x) ≤ C p(x) for all x with p(x) ≠ 0.

Русский

Если q ограничено сверху С умножить на p на оболочке, тогда q(x) ≤ C p(x) для всех x с p(x) ≠ 0.

LaTeX

$$$ q(x) \\le C \\cdot p(x) \\quad \\text{whenever } p(x) \\neq 0, \\text{ given shell bound relations}. $$$

Lean4

theorem continuous_of_le [TopologicalSpace E] [IsTopologicalAddGroup E] {p q : Seminorm 𝕝 E} (hq : Continuous q)
    (hpq : p ≤ q) : Continuous p :=
  by
  refine
    Seminorm.continuous_of_forall
      (fun r hr ↦ Filter.mem_of_superset (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))
  rw [ball_zero_eq]
  exact isOpen_lt hq continuous_const

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