IsBounded — Mathlib

English

For fixed output q and p-family, IsBounded(p, q, f) is equivalent to a condition with constants relative to p.

Русский

Для фиксированного q и p-семейства IsBounded эквивалентно условию с константами по p.

LaTeX

$$IsBounded p q f ↔ ∀ i, ∃ C, (q i).comp f ≤ C • p$$

Lean4

/-- The proposition that a linear map is bounded between spaces with families of seminorms. -/
def IsBounded (p : ι → Seminorm 𝕜 E) (q : ι' → Seminorm 𝕜₂ F) (f : E →ₛₗ[σ₁₂] F) : Prop :=
  ∀ i, ∃ s : Finset ι, ∃ C : ℝ≥0, (q i).comp f ≤ C • s.sup p

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