case a
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ e.source ∈ ⋃ (e : LocalEquiv M H) (_ : e ∈ c.atlas) (s : Set H) (_ : IsOpen s), {↑e ⁻¹' s ∩ e.source}
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ IsOpen e.source
apply TopologicalSpace.GenerateOpen.basic
case a
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ ∃ i, i ∈ c.atlas ∧ ∃ i_1, IsOpen i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source
case a
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ e.source ∈ ⋃ (e : LocalEquiv M H) (_ : e ∈ c.atlas) (s : Set H) (_ : IsOpen s), {↑e ⁻¹' s ∩ e.source}
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
case a
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ e.source = ↑e ⁻¹' univ ∩ e.source
case a
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ ∃ i, i ∈ c.atlas ∧ ∃ i_1, IsOpen i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source
refine' ⟨e, he, univ, isOpen_univ, _⟩
no goals
case a
H : Type u
H' : Type ?u.56289
M : Type u_1
M' : Type ?u.56295
M'' : Type ?u.56298
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ e.source = ↑e ⁻¹' univ ∩ e.source
simp only [Set.univ_inter, Set.preimage_univ]