ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Set ι<VAR>f : ι → Set X<VAR>hs : s.Finite<VAR>hf : ∀ i ∈ s, IsCompact (f i)<GOAL>IsCompact (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Finset ι<VAR>f : ι → Set X<VAR>hf : ∀ i ∈ s, IsCompact (f i)<GOAL>IsCompact (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>K : ℕ → Set X<VAR>hK : ∀ (n : ℕ), IsCompact (K n)<VAR>n : ℕ<GOAL>IsCompact (Set.Accumulate K n)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hf : S.Finite<VAR>hc : ∀ s ∈ S, IsCompact s<GOAL>IsCompact (⋃₀ S)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Sort u_2<VAR>f : ι → Set X<VAR>Finite ι<VAR>h : ∀ (i : ι), IsCompact (f i)<GOAL>IsCompact (⋃ i, f i)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>IsCompact s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology X<VAR>hs : IsCompact s<GOAL>s.Finite
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology X<GOAL>IsCompact s ↔ s.Finite
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s ∪ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>a : X<GOAL>IsCompact (insert a s)
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_cpct : ∀ (i : ι), IsCompact (V i)<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<GOAL>∃ i, V i ⊆ U
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>b : ι → Set X<VAR>hb : TopologicalSpace.IsTopologicalBasis (Set.range b)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<GOAL>∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>b : Set (Set X)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<GOAL>∃ s, U = ⋃₀ (Subtype.val '' ↑s)
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>b : ι → Set X<VAR>hb : TopologicalSpace.IsTopologicalBasis (Set.range b)<VAR>hb' : ∀ (i : ι), IsCompact (b i)<VAR>U : Set X<GOAL>IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.cocompact X).HasBasis IsCompact compl
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<GOAL>sᶜ ∈ Filter.cocompact X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Filter.cocompact X ≤ Filter.cofinite
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>DiscreteTopology X<GOAL>Filter.cocompact X = Filter.cofinite
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>f : Filter X<GOAL>Disjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>f : Filter X<GOAL>Disjoint f (Filter.cocompact X) ↔ ∃ K ∈ f, IsCompact K
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>y : Y<VAR>hf : Filter.Tendsto f (Filter.cocompact X) (𝓝 y)<VAR>hfc : Continuous f<GOAL>IsCompact (insert y (Set.range f))
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>f : ι → X<VAR>x : X<VAR>hf : Filter.Tendsto f Filter.cofinite (𝓝 x)<GOAL>IsCompact (insert x (Set.range f))
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>f : ℕ → X<VAR>x : X<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 x)<GOAL>IsCompact (insert x (Set.range f))
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.coclosedCompact X).HasBasis (fun s => IsClosed s ∧ IsCompact s) compl
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coclosedCompact X ↔ IsCompact (closure sᶜ)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coclosedCompact X ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ tᶜ ⊆ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>s ∈ Filter.coclosedCompact X ↔ ∃ t, IsClosed t ∧ IsCompact t ∧ sᶜ ⊆ t
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>sᶜ ∈ Filter.coclosedCompact X ↔ IsCompact (closure s)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>Filter.cocompact X ≤ Filter.coclosedCompact X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>hs' : IsClosed s<GOAL>sᶜ ∈ Filter.coclosedCompact X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>Bornology.IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : Filter Y<VAR>hs : IsCompact s<VAR>hf : Disjoint f (Filter.cocompact Y)<GOAL>𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ Set.univ)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>t : Set X<VAR>f : Filter X<VAR>ht : IsCompact t<VAR>hf : Disjoint f (Filter.cocompact X)<GOAL>f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (Set.univ ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>hs : IsCompact s<VAR>t : Set Y<VAR>ht : IsCompact t<VAR>n : Set (X × Y)<VAR>hn : IsOpen n<VAR>hp : s ×ˢ t ⊆ n<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsCompact Set.univ ↔ CompactSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>h : CompactSpace X<GOAL>IsCompact Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>f : Filter X<VAR>f.NeBot<GOAL>∃ x, ClusterPt x f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>F : Ultrafilter X<GOAL>↑F ≤ 𝓝 F.lim
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, ⋃ x ∈ t, U x = ⊤
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u, ⋂ i ∈ u, t i = ∅<GOAL>CompactSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>CompactSpace X<VAR>h : IsClosed s<GOAL>IsCompact s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>l : Filter X<VAR>y : X<VAR>h : ∀ (x : X), ClusterPt x l → x = y<GOAL>l ≤ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>l : Filter Y<VAR>y : X<VAR>f : Y → X<VAR>h : ∀ (x : X), MapClusterPt x l f → x = y<GOAL>Filter.Tendsto f l (𝓝 y)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NoncompactSpace X<GOAL>¬IsCompact Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>NoncompactSpace X<VAR>hs : IsCompact s<GOAL>s ≠ Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<GOAL>Filter.cocompact X = ⊥
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.cocompact X).NeBot → NoncompactSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>(Filter.cocompact X).NeBot ↔ NoncompactSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>¬CompactSpace X ↔ NoncompactSpace X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>DiscreteTopology X<GOAL>Finite X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s K : Set X<VAR>hs : s.Infinite<VAR>hK : IsCompact K<VAR>hsub : s ⊆ K<GOAL>∃ x ∈ K, AccPt x (Filter.cofinite ⊓ 𝓟 s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s K : Set X<VAR>hs : s.Infinite<VAR>hK : IsCompact K<VAR>hsub : s ⊆ K<GOAL>∃ x ∈ K, AccPt x (𝓟 s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>CompactSpace X<VAR>hs : s.Infinite<GOAL>∃ x, AccPt x (Filter.cofinite ⊓ 𝓟 s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>CompactSpace X<VAR>hs : s.Infinite<GOAL>∃ x, AccPt x (𝓟 s)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>Infinite X<GOAL>∃ z, (𝓝[≠] z).NeBot
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, ⋃ x ∈ t, interior (U x) = Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<GOAL>∃ t, ⋃ x ∈ t, U x = Set.univ
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<GOAL>{i | (f i).Nonempty}.Finite
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hne : ∀ (i : ι), (f i).Nonempty<GOAL>Set.univ.Finite
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>Filter.comap f (Filter.cocompact Y) ≤ Filter.cocompact X
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsCompact (Set.range f)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<GOAL>IsCompact (Set.diagonal X)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace X<GOAL>IsClosedMap Prod.snd
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<GOAL>IsClosedMap Prod.fst
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>Nonempty ι<VAR>V : ι → Set X<VAR>hV : Directed (fun x x_1 => x ⊇ x_1) V<VAR>hV_closed : ∀ (i : ι), IsClosed (V i)<VAR>U : Set X<VAR>hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x<GOAL>∃ i, V i ⊆ U
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsCompact s ↔ IsCompact (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>IsCompact s ↔ IsCompact (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsClosed (Set.range f)<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>IsCompact (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>K : Set Y<VAR>Kf : K ⊆ Set.range f<GOAL>IsCompact (f ⁻¹' K) ↔ IsCompact K
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>Kf : K ⊆ Set.range f<GOAL>IsCompact (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<VAR>K : Set Y<VAR>hK : IsCompact K<GOAL>IsCompact (f ⁻¹' K)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>Filter.Tendsto f (Filter.cocompact X) (Filter.cocompact Y)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>s : Set { x // p x }<GOAL>IsCompact s ↔ IsCompact (Subtype.val '' s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsCompact s ↔ IsCompact Set.univ
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsCompact s ↔ CompactSpace ↑s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>hs' : DiscreteTopology ↑s<GOAL>s.Finite
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>hs' : s.Infinite<GOAL>∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).NeBot
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>NoncompactSpace X<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>NoncompactSpace Y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : CompactSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>CompactSpace X
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>t : Set Y<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (s ×ˢ t)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>(Filter.cocompact X).coprod (Filter.cocompact Y) = Filter.cocompact (X × Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>NoncompactSpace (X × Y) ↔ NoncompactSpace X ∧ Nonempty Y ∨ Nonempty X ∧ NoncompactSpace Y
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<GOAL>(∀ (i : ι), IsCompact (s i)) → IsCompact {x | ∀ (i : ι), x i ∈ s i}
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<VAR>h : ∀ (i : ι), IsCompact (s i)<GOAL>IsCompact (Set.univ.pi s)
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>s : Set ((i : ι) → X i)<VAR>hs : IsClosed s<GOAL>IsCompact s ↔ ∀ (i : ι), IsCompact (Function.eval i '' s)
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>(i : ι) → TopologicalSpace (X i)<VAR>s : Set ((i : ι) → X i)<GOAL>(∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ Function.eval i ⁻¹' Ki
<VAR>ι : Type u_1<VAR>X : ι → Type u_3<VAR>(d : ι) → TopologicalSpace (X d)<GOAL>(Filter.coprodᵢ fun d => Filter.cocompact (X d)) = Filter.cocompact ((d : ι) → X d)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>S : Set X<VAR>hS : IsClosed S<VAR>hne : S.Nonempty<GOAL>∃ V ⊆ S, V.Nonempty ∧ IsClosed V ∧ ∀ V' ⊆ V, V'.Nonempty → IsClosed V' → V' = V
<VAR>self : TopCommRingCat<GOAL>TopologicalRing self.α
<VAR>X : Type u<VAR>CommRing X<VAR>TopologicalSpace X<VAR>TopologicalRing X<GOAL>(TopCommRingCat.of X).α = X
<VAR>X : TopCat<VAR>x : ↑X<VAR>U : TopologicalSpace.Opens ↑X<VAR>p : x ∈ U<GOAL>(TopologicalSpace.OpenNhds.inclusion x).obj { obj := U, property := p } = U
<VAR>X : TopCat<VAR>x : ↑X<VAR>U : TopologicalSpace.OpenNhds x<GOAL>OpenEmbedding ⇑U.obj.inclusion
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>x : ↑X<VAR>U : TopologicalSpace.Opens ↑Y<VAR>q : f x ∈ U<GOAL>(TopologicalSpace.OpenNhds.map f x).obj { obj := U, property := q } = { obj := (TopologicalSpace.Opens.map f).obj U, property := q }
<VAR>X : TopCat<VAR>x : ↑X<VAR>U : TopologicalSpace.OpenNhds ((𝟙 X) x)<GOAL>(TopologicalSpace.OpenNhds.map (𝟙 X) x).obj U = U
<VAR>X : TopCat<VAR>x : ↑X<VAR>U : Set ↑X<VAR>p : IsOpen U<VAR>q : (𝟙 X) x ∈ { carrier := U, is_open' := p }<GOAL>(TopologicalSpace.OpenNhds.map (𝟙 X) x).obj { obj := { carrier := U, is_open' := p }, property := q } = { obj := { carrier := U, is_open' := p }, property := q }
<VAR>X : TopCat<VAR>x : ↑X<VAR>U : (TopologicalSpace.OpenNhds x)ᵒᵖ<GOAL>(TopologicalSpace.OpenNhds.map (𝟙 X) x).obj (Opposite.unop U) = Opposite.unop U
<VAR>X : TopCat<VAR>x : ↑X<VAR>U : (TopologicalSpace.OpenNhds x)ᵒᵖ<GOAL>(TopologicalSpace.OpenNhds.map (𝟙 X) x).op.obj U = U
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>∀ (X_1 : TopologicalSpace.OpenNhds (f x)), (TopologicalSpace.OpenNhds.inclusionMapIso f x).hom.app X_1 = 𝟙 ((TopologicalSpace.Opens.map f).obj ((TopologicalSpace.OpenNhds.inclusion (f x)).obj X_1))
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>∀ (X_1 : TopologicalSpace.OpenNhds (f x)), (TopologicalSpace.OpenNhds.inclusionMapIso f x).inv.app X_1 = 𝟙 ((TopologicalSpace.OpenNhds.inclusion x).obj ((TopologicalSpace.OpenNhds.map f x).obj X_1))
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>(TopologicalSpace.OpenNhds.inclusionMapIso f x).hom = 𝟙 (TopologicalSpace.OpenNhds.inclusion (f x) ⋙ TopologicalSpace.Opens.map f)
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>x : ↑X<GOAL>(TopologicalSpace.OpenNhds.inclusionMapIso f x).inv = 𝟙 (TopologicalSpace.OpenNhds.map f x ⋙ TopologicalSpace.OpenNhds.inclusion x)
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>h : IsOpenMap ⇑f<VAR>x : ↑X<VAR>U : TopologicalSpace.OpenNhds x<GOAL>((h.functorNhds x).obj U).obj = h.functor.obj U.obj
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>h : IsOpenMap ⇑f<VAR>x : ↑X<GOAL>∀ {X_1 Y_1 : TopologicalSpace.OpenNhds x} (i : X_1 ⟶ Y_1), (h.functorNhds x).map i = h.functor.map i
<VAR>X : Type w<VAR>TopologicalSpace X<VAR>Y : Type u_1<VAR>t : TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)<GOAL>Continuous f
<VAR>X : Type w<VAR>t : TopologicalSpace X<VAR>self : UCompactlyGeneratedSpace X<GOAL>t ≤ TopologicalSpace.compactlyGenerated X
<VAR>X : Type w<VAR>t : TopologicalSpace X<VAR>UCompactlyGeneratedSpace X<GOAL>t = TopologicalSpace.compactlyGenerated X
<VAR>X : Type w<VAR>TopologicalSpace X<VAR>UCompactlyGeneratedSpace X<VAR>Y : Type u_1<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)<GOAL>Continuous f
<VAR>X : Type w<VAR>t : TopologicalSpace X<VAR>h : ∀ {Y : Type w} [tY : TopologicalSpace Y] (f : X → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f<GOAL>UCompactlyGeneratedSpace X
<VAR>self : CompactlyGenerated<GOAL>UCompactlyGeneratedSpace ↑self.toTop
<VAR>self : CompactlyGenerated<GOAL>CompactlyGenerated.compactlyGeneratedToTop.obj self = self.toTop
<GOAL>∀ {X Y : CategoryTheory.InducedCategory TopCat CompactlyGenerated.toTop} (f : X ⟶ Y), CompactlyGenerated.compactlyGeneratedToTop.map f = f
<VAR>X Y : CompactlyGenerated<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>(CompactlyGenerated.isoOfHomeo f).inv = { toFun := ⇑f.symm, continuous_toFun := ⋯ }
<VAR>X Y : CompactlyGenerated<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>(CompactlyGenerated.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }
<VAR>X Y : CompactlyGenerated<VAR>f : X ≅ Y<VAR>a : (CategoryTheory.forget CompactlyGenerated).obj Y<GOAL>(CompactlyGenerated.homeoOfIso f).symm a = f.inv a
<VAR>X Y : CompactlyGenerated<VAR>f : X ≅ Y<VAR>a : (CategoryTheory.forget CompactlyGenerated).obj X<GOAL>(CompactlyGenerated.homeoOfIso f) a = f.hom a
<VAR>X Y : CompactlyGenerated<VAR>f : X ≅ Y<GOAL>CompactlyGenerated.isoEquivHomeo f = CompactlyGenerated.homeoOfIso f
<VAR>X Y : CompactlyGenerated<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>CompactlyGenerated.isoEquivHomeo.symm f = CompactlyGenerated.isoOfHomeo f
<VAR>B X : Profinite<VAR>π : X ⟶ B<GOAL>[CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑π].TFAE
<VAR>α : Type<VAR>Finite α<VAR>B : Profinite<VAR>X : α → Profinite<VAR>π : (a : α) → X a ⟶ B<GOAL>[CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (π a) x = b].TFAE
<VAR>α : Type<VAR>Finite α<VAR>B : Profinite<VAR>X : α → Profinite<VAR>π : (a : α) → X a ⟶ B<VAR>surj : ∀ (b : ↑B.toTop), ∃ a x, (π a) x = b<GOAL>CategoryTheory.EffectiveEpiFamily X π
<VAR>α : Type u_1<VAR>Order.Frame α<GOAL>↑(Opposite.unop (Locale.of α)) = α
<VAR>X : TopCat<GOAL>topToLocale.obj X = Opposite.op (Frm.of (TopologicalSpace.Opens ↑X))
<GOAL>∀ {X Y : TopCat} (f : X ⟶ Y), topToLocale.map f = Quiver.Hom.op (TopologicalSpace.Opens.comap f)
<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), Nonempty ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<GOAL>(TopCat.partialSections F H).Nonempty
<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<GOAL>Directed Superset fun G => TopCat.partialSections F G.snd
<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<VAR>∀ (j : J), T2Space ↑(F.obj j)<VAR>G : Finset J<VAR>H : Finset (TopCat.FiniteDiagramArrow G)<GOAL>IsClosed (TopCat.partialSections F H)
<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>F : J ⥤ TopCat<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>∀ (j : J), Nonempty ↑(F.obj j)<VAR>∀ (j : J), CompactSpace ↑(F.obj j)<VAR>∀ (j : J), T2Space ↑(F.obj j)<GOAL>Nonempty ↑(TopCat.limitCone F).pt
<VAR>N : Type u_1<VAR>DecidableEq N<VAR>i : N<VAR>t₀ : ↑I<VAR>t : { j // j ≠ i } → ↑I<VAR>H : (t₀ = 0 ∨ t₀ = 1) ∨ t ∈ Cube.boundary { j // j ≠ i }<GOAL>(Cube.insertAt i) (t₀, t) ∈ Cube.boundary N
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f g : ↑(Ω^ N X x)<VAR>H : ∀ (y : N → ↑I), f y = g y<GOAL>f = g
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f : C(N → ↑I, X)<VAR>H : f ∈ Ω^ N X x<VAR>y : N → ↑I<GOAL>⟨f, H⟩ y = f y
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f : ↑(Ω^ N X x)<VAR>g : (N → ↑I) → X<VAR>h : g = ⇑f<GOAL>⇑(GenLoop.copy f g h) = g
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f : ↑(Ω^ N X x)<VAR>g : (N → ↑I) → X<VAR>h : g = ⇑f<GOAL>GenLoop.copy f g h = f
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f : ↑(Ω^ N X x)<VAR>y : N → ↑I<GOAL>y ∈ Cube.boundary N → f y = x
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>t : N → ↑I<GOAL>GenLoop.const t = x
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f : ↑(Ω^ N X x)<GOAL>GenLoop.Homotopic f f
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f g : ↑(Ω^ N X x)<VAR>H : GenLoop.Homotopic f g<GOAL>GenLoop.Homotopic g f
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>f g h : ↑(Ω^ N X x)<VAR>H0 : GenLoop.Homotopic f g<VAR>H1 : GenLoop.Homotopic g h<GOAL>GenLoop.Homotopic f h
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<GOAL>Equivalence GenLoop.Homotopic
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>t : ↑I<GOAL>↑((GenLoop.toLoop i p) t) = ((↑p).comp (Cube.insertAt i).toContinuousMap).curry t
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<GOAL>Continuous (GenLoop.toLoop i)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) GenLoop.const<GOAL>↑(GenLoop.fromLoop i p) = ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp (Cube.splitAt i).toContinuousMap
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<GOAL>Continuous (GenLoop.fromLoop i)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) GenLoop.const<GOAL>GenLoop.toLoop i (GenLoop.fromLoop i p) = p
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<GOAL>(GenLoop.loopHomeo i) p = GenLoop.toLoop i p
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) GenLoop.const<GOAL>(GenLoop.loopHomeo i).symm p = GenLoop.fromLoop i p
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>t : ↑I<VAR>tn : { j // j ≠ i } → ↑I<GOAL>((GenLoop.toLoop i p) t) tn = p ((Cube.insertAt i) (t, tn))
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) GenLoop.const<VAR>t : N → ↑I<GOAL>(GenLoop.fromLoop i p) t = (p (t i)) ((Cube.splitAt i) t).2
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t : ↑I × ↑I<VAR>tₙ : { j // j ≠ i } → ↑I<GOAL>((GenLoop.homotopyTo i H) t) tₙ = H (t.1, (Cube.insertAt i) (t.2, tₙ))
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>GenLoop.Homotopic p q → Path.Homotopic (GenLoop.toLoop i p) (GenLoop.toLoop i q)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q)<GOAL>∀ (a : ↑I × (N → ↑I)), (GenLoop.homotopyFrom i H) a = Function.uncurry (fun x_1 y => Function.uncurry (fun x_2 y => ↑(H (x_1, x_2)) y) y) (Prod.map id (⇑(Cube.splitAt i).toContinuousMap) a)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>Path.Homotopic (GenLoop.toLoop i p) (GenLoop.toLoop i q) → GenLoop.Homotopic p q
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i j : N<VAR>h : i ≠ j<VAR>a b c d : ↑(Ω^ N X x)<GOAL>GenLoop.transAt i (GenLoop.transAt j a b) (GenLoop.transAt j c d) = GenLoop.transAt j (GenLoop.transAt i a c) (GenLoop.transAt i b d)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>GenLoop.fromLoop i (Path.trans (GenLoop.toLoop i p) (GenLoop.toLoop i q)) = GenLoop.transAt i p q
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>x : X<VAR>DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<GOAL>GenLoop.fromLoop i (Path.symm (GenLoop.toLoop i p)) = GenLoop.symmAt i p