t2Space_of_covering — Mathlib

English

If 𝔖 covers α, the topology on α →ᵤ[𝔖] β is T2 whenever β is T2.

Русский

Если 𝔖 покрывает α, топология на α →ᵤ[𝔖] β является T2, когда β — T2.

LaTeX

$$If [T2Space β] and ⋃₀ 𝔖 = univ, then T2Space (α →ᵤ[𝔖] β).$$

Lean4

/-- If `𝔖` covers `α`, then the topology of `𝔖`-convergence is T₂. -/
theorem t2Space_of_covering [T2Space β] (h : ⋃₀ 𝔖 = univ) : T2Space (α →ᵤ[𝔖] β) where
  t2 f g
    hfg := by
    obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)
    obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)
    exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

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