English
The induced embedding from principal inclusion into the top structure is an embedding.
Русский
Включение по принципу в топологической структуре является вложением.
LaTeX
$$$\\text{IsEmbedding}(\\text{RestrictedProduct.inclusion } R A hS)$$$
Lean4
/-- If each `R i` is weakly locally compact, each `A i` is open, and all but finitely many `A i`s
are also compact, then the restricted product `Πʳ i, [R i, A i]` is weakly locally compact. -/
theorem weaklyLocallyCompactSpace_of_cofinite [∀ i, WeaklyLocallyCompactSpace (R i)]
(hAcompact : ∀ᶠ i in cofinite, IsCompact (A i)) : WeaklyLocallyCompactSpace (Πʳ i, [R i, A i]) where
exists_compact_mem_nhds := fun x ↦ by
set S := {i | IsCompact (A i) ∧ x i ∈ A i}
have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr (hAcompact.and x.2)
have hSx : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi.2
have hSA : ∀ i ∈ S, IsCompact (A i) := fun i hi ↦ hi.1
haveI := weaklyLocallyCompactSpace_of_principal hS hSA
rcases exists_inclusion_eq_of_eventually R A hS hSx with ⟨x', hxx'⟩
rw [← hxx', nhds_eq_map_inclusion hAopen]
rcases exists_compact_mem_nhds x' with ⟨K, K_compact, hK⟩
exact ⟨inclusion R A hS '' K, K_compact.image (continuous_inclusion hS), image_mem_map hK⟩
