H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.49347
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
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' t
⊢ y ∈ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.49347
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
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
⊢ LiftPropWithinAt P g t x
refine' ⟨h.1.mono hts, mono (fun y hy ↦ _) h.2⟩
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.49347
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
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : ↑(LocalHomeomorph.symm (chartAt H x)) y ∈ t
⊢ y ∈ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.49347
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
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : y ∈ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' t
⊢ y ∈ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s
simp only [mfld_simps] at hy
no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.49347
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
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropWithinAt P g s x
hts : t ⊆ s
y : H
hy : ↑(LocalHomeomorph.symm (chartAt H x)) y ∈ t
⊢ y ∈ ↑(LocalHomeomorph.symm (chartAt H x)) ⁻¹' s
simp only [hy, hts _, mfld_simps]