ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : X → M'<VAR>e : PartialHomeomorph X H<VAR>x : X<VAR>s : Set X<VAR>xe : x ∈ e.source<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ StructureGroupoid.maximalAtlas M G<VAR>xe' : x ∈ e'.source<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e : PartialHomeomorph M H<VAR>f : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>HasGroupoid M G<VAR>HasGroupoid M' G'<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e : PartialHomeomorph M H<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>HasGroupoid M G<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>xe : x ∈ e.source<GOAL>ChartedSpace.LiftPropWithinAt P g s x ↔ ChartedSpace.LiftPropWithinAt P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>f : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>HasGroupoid M' G'<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g) s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e : PartialHomeomorph M H<VAR>f : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>HasGroupoid M G<VAR>HasGroupoid M' G'<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>ChartedSpace.LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ ChartedSpace.LiftPropWithinAt P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e : PartialHomeomorph M H<VAR>f : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>hG : G.LocalInvariantProp G' P<VAR>HasGroupoid M G<VAR>HasGroupoid M' G'<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>h : ChartedSpace.LiftPropOn P g s<VAR>y : H<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (s ∩ g ⁻¹' f.source)<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) y
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s t : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>ht : t ∈ 𝓝[s] x<GOAL>ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s t : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>ht : t ∈ 𝓝 x<GOAL>ChartedSpace.LiftPropWithinAt P g (s ∩ t) x ↔ ChartedSpace.LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ChartedSpace.LiftPropWithinAt P g s x<VAR>hs : s ∈ 𝓝 x<GOAL>ChartedSpace.LiftPropAt P g x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ChartedSpace.LiftPropAt P g x<VAR>hs : s ∈ 𝓝 x<GOAL>ChartedSpace.LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g (s ∩ u)<GOAL>ChartedSpace.LiftPropOn P g s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g u<GOAL>ChartedSpace.LiftProp P g
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ChartedSpace.LiftPropWithinAt P g s x<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>ChartedSpace.LiftPropWithinAt P g' s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h₁ : g' =ᶠ[𝓝[s] x] g<VAR>hx : g' x = g x<GOAL>ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h₁ : ∀ y ∈ s, g' y = g y<VAR>hx : g' x = g x<GOAL>ChartedSpace.LiftPropWithinAt P g' s x ↔ ChartedSpace.LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ChartedSpace.LiftPropWithinAt P g s x<VAR>h₁ : ∀ y ∈ s, g' y = g y<VAR>hx : g' x = g x<GOAL>ChartedSpace.LiftPropWithinAt P g' s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h₁ : g' =ᶠ[𝓝 x] g<GOAL>ChartedSpace.LiftPropAt P g' x ↔ ChartedSpace.LiftPropAt P g x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ChartedSpace.LiftPropAt P g x<VAR>h₁ : g' =ᶠ[𝓝 x] g<GOAL>ChartedSpace.LiftPropAt P g' x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s : Set M<VAR>hG : G.LocalInvariantProp G' P<VAR>h : ChartedSpace.LiftPropOn P g s<VAR>h₁ : ∀ y ∈ s, g' y = g y<GOAL>ChartedSpace.LiftPropOn P g' s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s : Set M<VAR>hG : G.LocalInvariantProp G' P<VAR>h₁ : ∀ y ∈ s, g' y = g y<GOAL>ChartedSpace.LiftPropOn P g' s ↔ ChartedSpace.LiftPropOn P g s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s t : Set M<VAR>x : M<VAR>mono_of_mem : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x<VAR>h : ChartedSpace.LiftPropWithinAt P g s x<VAR>hst : s ∈ 𝓝[t] x<GOAL>ChartedSpace.LiftPropWithinAt P g t x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s t : Set M<VAR>x : M<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : ChartedSpace.LiftPropWithinAt P g s x<VAR>hts : t ⊆ s<GOAL>ChartedSpace.LiftPropWithinAt P g t x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>x : M<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : ChartedSpace.LiftPropAt P g x<GOAL>ChartedSpace.LiftPropWithinAt P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s t : Set M<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : ChartedSpace.LiftPropOn P g t<VAR>hst : s ⊆ t<GOAL>ChartedSpace.LiftPropOn P g s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>s : Set M<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : ChartedSpace.LiftProp P g<GOAL>ChartedSpace.LiftPropOn P g s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph M H<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>hx : x ∈ e.source<GOAL>ChartedSpace.LiftPropAt Q (↑e) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph M H<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<GOAL>ChartedSpace.LiftPropOn Q (↑e) e.source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph M H<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>x : H<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>hx : x ∈ e.target<GOAL>ChartedSpace.LiftPropAt Q (↑e.symm) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e : PartialHomeomorph M H<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<GOAL>ChartedSpace.LiftPropOn Q (↑e.symm) e.target
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<GOAL>ChartedSpace.LiftPropAt Q (↑(chartAt H x)) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<GOAL>ChartedSpace.LiftPropOn Q (↑(chartAt H x)) (chartAt H x).source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<GOAL>ChartedSpace.LiftPropAt Q (↑(chartAt H x).symm) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<GOAL>ChartedSpace.LiftPropOn Q (↑(chartAt H x).symm) (chartAt H x).target
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>f : PartialHomeomorph H H<VAR>hf : f ∈ G<VAR>x : H<VAR>hx : x ∈ f.source<GOAL>ChartedSpace.LiftPropAt Q (↑f) x
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>f : PartialHomeomorph H H<VAR>hf : f ∈ G<GOAL>ChartedSpace.LiftPropOn Q (↑f) f.source
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<GOAL>ChartedSpace.LiftProp Q id
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>U : TopologicalSpace.Opens M<VAR>f : M → M'<VAR>x : ↥U<GOAL>ChartedSpace.LiftPropAt P f ↑x ↔ ChartedSpace.LiftPropAt P (f ∘ Subtype.val) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>U V : TopologicalSpace.Opens M<VAR>hUV : U ≤ V<VAR>f : ↥V → M'<VAR>x : ↥U<GOAL>ChartedSpace.LiftPropAt P f (Set.inclusion hUV x) ↔ ChartedSpace.LiftPropAt P (f ∘ Set.inclusion hUV) x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>U : TopologicalSpace.Opens M<GOAL>ChartedSpace.LiftProp Q Subtype.val
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id Set.univ y<VAR>U V : TopologicalSpace.Opens M<VAR>hUV : U ≤ V<GOAL>ChartedSpace.LiftProp Q (Set.inclusion hUV)
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<GOAL>G.LocalInvariantProp G G.IsLocalStructomorphWithinAt
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>s : Set H<VAR>x : H<VAR>hx : x ∈ f.source ∪ sᶜ<GOAL>G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>s : Set H<VAR>x : H<VAR>hs : f.source ⊆ s<VAR>hx : x ∈ f.source ∪ sᶜ<GOAL>G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
<VAR>H : Type u_1<VAR>TopologicalSpace H<VAR>G : StructureGroupoid H<VAR>ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>x : H<GOAL>G.IsLocalStructomorphWithinAt (↑f) f.source x ↔ x ∈ f.source → ∃ e ∈ G, e.source ⊆ f.source ∧ Set.EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
<VAR>H₁ : Type u_6<VAR>TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>TopologicalSpace H₃<VAR>ChartedSpace H₁ H₂<VAR>ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>HasGroupoid H₂ G₁<VAR>ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, ChartedSpace.LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<GOAL>HasGroupoid H₃ G₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : AlgebraicGeometry.SheafedSpace C<GOAL>self.presheaf.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>carrier : TopCat<VAR>presheaf : TopCat.Presheaf C carrier<VAR>h : { carrier := carrier, presheaf := presheaf }.presheaf.IsSheaf<GOAL>↑{ carrier := carrier, presheaf := presheaf, IsSheaf := h }.toPresheafedSpace = carrier
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>α β : X ⟶ Y<VAR>w : α.base = β.base<VAR>h : α.c ≫ CategoryTheory.whiskerRight (CategoryTheory.eqToHom ⋯) X.presheaf = β.c<GOAL>α = β
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>e : X.toPresheafedSpace ≅ Y.toPresheafedSpace<GOAL>(AlgebraicGeometry.SheafedSpace.isoMk e).hom = e.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>e : X.toPresheafedSpace ≅ Y.toPresheafedSpace<GOAL>(AlgebraicGeometry.SheafedSpace.isoMk e).inv = e.inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : AlgebraicGeometry.SheafedSpace C<GOAL>AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj self = self.toPresheafedSpace
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.InducedCategory (AlgebraicGeometry.PresheafedSpace C) AlgebraicGeometry.SheafedSpace.toPresheafedSpace} (f : X ⟶ Y), AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.map f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.SheafedSpace C<GOAL>(𝟙 X).base = 𝟙 ↑X.toPresheafedSpace
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.SheafedSpace C<GOAL>(𝟙 X).c = CategoryTheory.eqToHom ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : AlgebraicGeometry.SheafedSpace C<VAR>U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<GOAL>(𝟙 X).c.app U = 𝟙 (X.presheaf.obj U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.SheafedSpace C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g).base = f.base ≫ g.base
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.SheafedSpace C<VAR>α : X ⟶ Y<VAR>β : Y ⟶ Z<VAR>U : (TopologicalSpace.Opens ↑↑Z.toPresheafedSpace)ᵒᵖ<GOAL>(α ≫ β).c.app U = β.c.app U ≫ α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj (Opposite.unop U)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : AlgebraicGeometry.SheafedSpace C<VAR>α : X ⟶ Y<VAR>β : Y ⟶ Z<VAR>U : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace<GOAL>(α ≫ β).c.app (Opposite.op U) = β.c.app (Opposite.op U) ≫ α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj U))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : AlgebraicGeometry.SheafedSpace C<VAR>α β : X ⟶ Y<VAR>h : α = β<VAR>U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ<GOAL>α.c.app U = β.c.app U ≫ X.presheaf.map (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>U : TopCat<VAR>X : AlgebraicGeometry.SheafedSpace C<VAR>f : U ⟶ ↑X.toPresheafedSpace<VAR>h : OpenEmbedding ⇑f<VAR>V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<GOAL>(X.ofRestrict h).c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op