locPathConnectedSpace — Mathlib

English

If e: Y → X is an open embedding and X is locally path-connected, then Y is locally path-connected (with the subspace topology).

Русский

Если e: Y → X — открытое вложение и X имеет локальную путевую связность, тогда Y с подпространственной топологией также локально путеподключено.

LaTeX

$$IsOpenEmbedding e → LocPathConnectedSpace Y$$

Lean4

theorem locPathConnectedSpace {e : Y → X} (he : IsOpenEmbedding e) : LocPathConnectedSpace Y :=
  have (y : Y) : (𝓝 y).HasBasis (fun s ↦ s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) (e ⁻¹' ·) :=
    he.basis_nhds <| pathConnected_subset_basis he.isOpen_range (mem_range_self _)
  .of_bases this fun x s ⟨_, hs, hse⟩ ↦ by rwa [he.isPathConnected_iff, image_preimage_eq_of_subset hse]

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