H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
hsc : Set.Countable s
this : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).toLocalEquiv.source
⊢ SecondCountableTopology M
H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
hsc : Set.Countable s
⊢ SecondCountableTopology M
haveI : ∀ x : M, SecondCountableTopology (chartAt H x).source :=
  fun x ↦ (chartAt (H := H) x).secondCountableTopology_source
H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
hsc : Set.Countable s
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).toLocalEquiv.source
this : Encodable ↑s
⊢ SecondCountableTopology M
H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
hsc : Set.Countable s
this : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).toLocalEquiv.source
⊢ SecondCountableTopology M
haveI := hsc.toEncodable
H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : ↑s), (chartAt H ↑x).toLocalEquiv.source) = univ
hsc : Set.Countable s
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).toLocalEquiv.source
this : Encodable ↑s
⊢ SecondCountableTopology M
H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : M) (_ : x ∈ s), (chartAt H x).toLocalEquiv.source) = univ
hsc : Set.Countable s
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).toLocalEquiv.source
this : Encodable ↑s
⊢ SecondCountableTopology M
rw [biUnion_eq_iUnion] at hs
no goals
H : Type u
H' : Type ?u.43633
M : Type u_1
M' : Type ?u.43639
M'' : Type ?u.43642
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SecondCountableTopology H
s : Set M
hs : (⋃ (x : ↑s), (chartAt H ↑x).toLocalEquiv.source) = univ
hsc : Set.Countable s
this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).toLocalEquiv.source
this : Encodable ↑s
⊢ SecondCountableTopology M
exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs