Theorems · Theorem · manifolds

ChartedSpace.secondCountable_of_countable_cover

∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  [SecondCountableTopology H] {s : Set M},
  ⋃ x ∈ s, (chartAt H x).source = Set.univ → s.Countable → SecondCountableTopology M

Defined in

Mathlib.Geometry.Manifold.ChartedSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceChartedSpaceSecondCountableTopology