instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space

English

If f is continuous, and s ∈ nhds(f(x)) and K is compact with K ∈ nhds(x), then there exists a compact L ∈ nhds(x) with MapsTo f L s.

Русский

Если f непрерывно, и s ∈ nhds(f(x)) и K компактно с K ∈ nhds(x), то существует компактная L ⊆ nhds(x) такая, что MapsTo f L s.

LaTeX

$$∃ L ∈ nhds(x), IsCompact L ∧ MapsTo f L s$$

Lean4

instance (priority := 900) {X Y : Type*} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [TopologicalSpace Y]
    [R1Space Y] : LocallyCompactPair X Y where
  exists_mem_nhds_isCompact_mapsTo hf
    hs :=
    let ⟨_K, hKc, hKx⟩ := exists_compact_mem_nhds _
    exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds hf hs hKc hKx

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