hasProdLocallyUniformlyOn_of_forall_compact

English

If s is open, β is locally compact, and for every compact K⊆s we have HasProdUniformlyOn f g {K}, then HasProdLocallyUniformlyOn f g s.

Русский

Если s открыто, β локально компактно, и для каждого компакта K⊆s выполнено HasProdUniformlyOn f g {K}, то HasProdLocallyUniformlyOn f g s.

LaTeX

$$$ IsOpen\ s \to [LocallyCompactSpace β] \to (\forall K\subset s, IsCompact K \to HasProdUniformlyOn f g {K}) \to HasProdLocallyUniformlyOn f g s $$$

Lean4

@[to_additive]
theorem hasProdLocallyUniformlyOn_of_forall_compact (hs : IsOpen s) [LocallyCompactSpace β]
    (h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g { K }) : HasProdLocallyUniformlyOn f g s :=
  by
  rw [HasProdLocallyUniformlyOn, tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
  simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h

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