English
Any space that is barrelled and a Baire space is barrelled; in particular Banach and Fréchet spaces.
Русский
Любое пространство, являющееся barrelled и Baire, является barrelled; в частности, пространства Банаха и Фреше.
LaTeX
$$instance\\ instBarrelledSpace [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜₁ E] [BaireSpace E] : BarrelledSpace 𝕜₁ E$$
Lean4
/-- Any TVS over a `NontriviallyNormedField` that is also a Baire space is barrelled. In
particular, this applies to Banach spaces and Fréchet spaces. -/
instance instBarrelledSpace [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜₁ E] [BaireSpace E] :
BarrelledSpace 𝕜₁ E where
continuous_of_lowerSemicontinuous := by
-- Let `p` be a lower-semicontinuous seminorm on `E`.
intro p hp
have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
eq_univ_of_forall fun x ↦
mem_iUnion.mpr
(exists_nat_ge <| p (x - 0))
-- Hence, one of them has nonempty interior. Let `n : ℕ` be its radius, and fix `x` an
-- interior point.
rcases nonempty_interior_of_iUnion_of_closed h₁ h₂ with
⟨n, ⟨x, hxn⟩⟩
-- To show that `p` is continuous, we will show that the `p`-closed-ball of
-- radius `2*n` is a neighborhood of zero.
refine Seminorm.continuous' (r := n + n) ?_
rw [p.closedBall_zero_eq] at hxn ⊢
have hxn' : p x ≤ n := by convert interior_subset hxn
rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn
filter_upwards [hxn] with y hy
calc
p y = p (x + y - x) := by rw [add_sub_cancel_left]
_ ≤ p (x + y) + p x := (map_sub_le_add _ _ _)
_ ≤ n + n := add_le_add hy hxn'
