H : Type u_2
M : Type u_1
H' : Type u_3
M' : Type u_4
X : Type ?u.39327
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftPropOn P g univ
H : Type u_2
M : Type u_1
H' : Type u_3
M' : Type u_4
X : Type ?u.39327
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftProp P g
rw [← liftPropOn_univ]
H : Type u_2
M : Type u_1
H' : Type u_3
M' : Type u_4
X : Type ?u.39327
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝¹ : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
x : M
x✝ : x ∈ univ
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)
H : Type u_2
M : Type u_1
H' : Type u_3
M' : Type u_4
X : Type ?u.39327
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftPropOn P g univ
refine' hG.liftPropOn_of_locally_liftPropOn fun x _ ↦ _
no goals
H : Type u_2
M : Type u_1
H' : Type u_3
M' : Type u_4
X : Type ?u.39327
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : LocalHomeomorph M H
f f' : LocalHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g g' : M → M'
s t : Set M
x✝¹ : M
Q : (H → H) → Set H → H → Prop
hG : LocalInvariantProp G G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
x : M
x✝ : x ∈ univ
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)
simp [h x]