English
Locally uniform on s is equivalent to a family of equivalent statements including compact basis, etc., for LocallyCompact spaces.
Русский
Локальная равномерность на s эквивалентна набору эквивалентных утверждений, включая базис компактных подмножеств, для локально-компактных пространств.
LaTeX
$$$$\text{LocallyUniformOn}_TFAE(F,g,p,s)$$$$
Lean4
theorem tendstoLocallyUniformlyOn_TFAE [LocallyCompactSpace α] (G : ι → α → β) (g : α → β) (p : Filter ι)
(hs : IsOpen s) :
List.TFAE
[TendstoLocallyUniformlyOn G g p s, ∀ K, K ⊆ s → IsCompact K → TendstoUniformlyOn G g p K,
∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v] :=
by
tfae_have 1 → 2
| h, K, hK1, hK2 => (tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK2).mp (h.mono hK1)
tfae_have 2 → 3
| h, x, hx => by
obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩
tfae_have 3 → 1
| h, u, hu, x, hx => by
obtain ⟨v, hv1, hv2⟩ := h x hx
exact ⟨v, hv1, hv2 u hu⟩
tfae_finish
