English
If every q_i∘f is continuous, then f is continuous (for the appropriate linear settings).
Русский
Если каждая композиция q_i∘f непрерывна, то сама f непрерывна.
LaTeX
$$$WithSeminorms q \\Rightarrow ∀ f, (∀ i, Continuous (q_i \\circ f)) \\Rightarrow Continuous f$$$
Lean4
/-- In a topological vector space, the topology is generated by a single seminorm `p` iff
the unit ball for this seminorm is a bounded neighborhood of `0`. -/
theorem withSeminorms_iff_mem_nhds_isVonNBounded [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
{p : Seminorm 𝕜 E} : WithSeminorms (fun (_ : Fin 1) ↦ p) ↔ p.ball 0 1 ∈ 𝓝 0 ∧ IsVonNBounded 𝕜 (p.ball 0 1) := by
/- The nontrivial direction is from right to left. With `SeminormFamily.withSeminorms_of_nhds`,
we need to see that the neighborhoods of zero for the initial topology and for `p` coincide. -/
refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
· apply (h.mem_nhds_iff _ _).2
exact ⟨Finset.univ, 1, zero_lt_one, by simp⟩
· apply h.isVonNBounded_iff_seminorm_bounded.2 (fun i ↦ ?_)
exact ⟨1, zero_lt_one, by simp⟩
rintro ⟨h, h'⟩
apply SeminormFamily.withSeminorms_of_nhds
ext s
refine ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩
· /- Show that a neighborhood `s` of zero for the topology is a neighborhood for `p`, by using the
boundedess of `p.ball 0 1`: this ensures that, for some nonzero `c`, we have
`p.ball 0 1 ⊆ c • s`, and therefore `p.ball 0 (‖c‖⁻¹) ⊆ s`. -/
obtain ⟨c, hc, c_ne⟩ : ∃ (c : 𝕜), p.ball 0 1 ⊆ c • s ∧ c ≠ 0 := ((h' hs).and (eventually_ne_cobounded 0)).exists
have : p.ball 0 (‖c⁻¹‖) ⊆ s :=
by
have : c • p.ball 0 (‖c⁻¹‖) ⊆ c • s := by simpa [smul_ball_zero c_ne, ← norm_mul, c_ne] using hc
rwa [smul_set_subset_smul_set_iff₀ c_ne] at this
apply Filter.mem_of_superset _ this
apply FilterBasis.mem_filter_of_mem
change p.ball 0 (‖c⁻¹‖) ∈ SeminormFamily.basisSets (fun (i : Fin 1) ↦ p)
apply SeminormFamily.basisSets_singleton_mem _ 0
simpa using c_ne
· /- Show that a neighborhood `s` for `p` is a neighborhood for the topology, by using the
fact that `p.ball 0 1` is a neighborhood of `0`. Indeed, `s` contains a ball `p.ball 0 r`,
which contains `c • p.ball 0 1` for some nonzero `c`. The latter set is a neighborhood of zero
for the topology thanks to the topological vector space assumption. -/
rcases (FilterBasis.mem_filter_iff _).1 hs with ⟨t, ht, ts⟩
suffices t ∈ 𝓝 0 from Filter.mem_of_superset this ts
rcases (SeminormFamily.basisSets_iff _).1 ht with ⟨w, r, r_pos, hw⟩
rcases eq_or_ne w ∅ with rfl | w_ne
· simp only [ball, Finset.sup_empty, sub_zero, coe_bot, Pi.zero_apply, r_pos, setOf_true] at hw
simp [hw]
have : t = p.ball 0 r :=
by
have : w = Finset.univ := by
rcases Finset.nonempty_of_ne_empty w_ne with ⟨i, hi⟩
ext j
simp only [Subsingleton.elim j i, hi, Finset.mem_univ]
simpa only [this, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, Finset.sup_singleton] using hw
rw [this]
obtain ⟨c, c_pos, hc⟩ : ∃ (c : 𝕜), 0 < ‖c‖ ∧ ‖c‖ < r := exists_norm_lt 𝕜 r_pos
have c_ne : c ≠ 0 := (by simpa using c_pos)
have : c • p.ball 0 1 ⊆ p.ball 0 r := by
rw [smul_ball_zero c_ne]
exact ball_mono (by simpa using hc.le)
apply Filter.mem_of_superset ?_ this
simpa using smul_mem_nhds_smul₀ c_ne h
