English
The AddGroupFilterBasis induced by p.basisSets is compatible with addition in E.
Русский
Добавляющий фильтр-база совместим с операцией сложения на E.
LaTeX
$$basisSets_add (U) (hU : U ∈ p.basisSets) : ∃ V ∈ p.basisSets, V + V ⊆ U$$
Lean4
theorem isBounded_sup {p : ι → Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F} (hf : IsBounded p q f)
(s' : Finset ι') : ∃ (C : ℝ≥0) (s : Finset ι), (s'.sup q).comp f ≤ C • s.sup p := by
classical
obtain rfl | _ := s'.eq_empty_or_nonempty
· exact ⟨1, ∅, by simp [Seminorm.bot_eq_zero]⟩
choose fₛ fC hf using hf
use s'.card • s'.sup fC, Finset.biUnion s' fₛ
have hs : ∀ i : ι', i ∈ s' → (q i).comp f ≤ s'.sup fC • (Finset.biUnion s' fₛ).sup p :=
by
intro i hi
refine (hf i).trans (smul_le_smul ?_ (Finset.le_sup hi))
exact Finset.sup_mono (Finset.subset_biUnion_of_mem fₛ hi)
refine (comp_mono f (finset_sup_le_sum q s')).trans ?_
simp_rw [← pullback_apply, map_sum, pullback_apply]
refine (Finset.sum_le_sum hs).trans ?_
rw [Finset.sum_const, smul_assoc]
