Theorems · Theorem · general topology

IsLocalHomeomorph.isTopologicalBasis

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f →
    TopologicalSpace.IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}

Ranges of continuous local sections of a local homeomorphism form a basis of the source space.

Defined in

Mathlib.Topology.IsLocalHomeomorph

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace