const_isBounded — Mathlib

English

The moduleFilterBasis on F is induced by the AddGroupFilterBasis from p and smul operations.

Русский

moduleFilterBasis для F индуцирован AddGroupFilterBasis от p и операций умножения.

LaTeX

$$protected def moduleFilterBasis : ModuleFilterBasis 𝕜 F$$

Lean4

theorem const_isBounded (ι : Type*) [Nonempty ι] {p : Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F) :
    IsBounded (fun _ : ι => p) q f ↔ ∀ i, ∃ C : ℝ≥0, (q i).comp f ≤ C • p :=
  by
  constructor <;> intro h i
  · rcases h i with ⟨s, C, h⟩
    exact ⟨C, le_trans h (smul_le_smul (Finset.sup_le fun _ _ => le_rfl) le_rfl)⟩
  use {Classical.arbitrary ι}
  simp only [h, Finset.sup_singleton]

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