isBounded_const — Mathlib

English

Equivalence of IsBounded when replacing p by a constant seminorm across i.

Русский

Эквивалентность IsBounded при замене p константной семинормой через i.

LaTeX

$$Eq (Seminorm.IsBounded p q f) (Exists (s) (Exists (C), q.comp f ≤ C • s.sup p))$$

Lean4

theorem isBounded_const (ι' : Type*) [Nonempty ι'] {p : ι → Seminorm 𝕜 E} {q : Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
    IsBounded p (fun _ : ι' => q) f ↔ ∃ (s : Finset ι) (C : ℝ≥0), q.comp f ≤ C • s.sup p := by
  simp only [IsBounded, forall_const]

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