Theorems · Theorem · general topology

pathConnected_subset_basis

∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} [LocallyPathConnectedSpace X] {U : Set X},
  IsOpen U → x ∈ U → (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s ∧ s ⊆ U) id

Defined in

Mathlib.Topology.Connected.LocallyPathConnected

Cited by

1 results in Mathlib

Foundations

Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLocallyPathConnectedSpace