ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_2<VAR>f : OnePoint X → α<VAR>l : Filter α<GOAL>Filter.Tendsto f (𝓝 OnePoint.infty) l ↔ Filter.Tendsto f (pure OnePoint.infty) l ∧ Filter.Tendsto (f ∘ OnePoint.some) (Filter.coclosedCompact X) l
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_2<VAR>f : OnePoint X → α<VAR>l : Filter α<GOAL>Filter.Tendsto f (𝓝 OnePoint.infty) l ↔ ∀ s ∈ l, f OnePoint.infty ∈ s ∧ ∃ t, IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : OnePoint X → Y<GOAL>ContinuousAt f OnePoint.infty ↔ Filter.Tendsto (f ∘ OnePoint.some) (Filter.coclosedCompact X) (𝓝 (f OnePoint.infty))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : OnePoint X → Y<GOAL>ContinuousAt f OnePoint.infty ↔ ∀ s ∈ 𝓝 (f OnePoint.infty), ∃ t, IsClosed t ∧ IsCompact t ∧ Set.MapsTo (f ∘ OnePoint.some) tᶜ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : OnePoint X → Y<VAR>x : X<GOAL>ContinuousAt f ↑x ↔ ContinuousAt (f ∘ OnePoint.some) x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : OnePoint X → Y<GOAL>Continuous f ↔ Filter.Tendsto (fun x => f ↑x) (Filter.coclosedCompact X) (𝓝 (f OnePoint.infty)) ∧ Continuous fun x => f ↑x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>DiscreteTopology X<VAR>f : OnePoint X → Y<GOAL>Continuous f ↔ Filter.Tendsto (fun x => f ↑x) Filter.cofinite (𝓝 (f OnePoint.infty))
<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : OnePoint ℕ → Y<GOAL>Continuous f ↔ Filter.Tendsto (fun x => f ↑x) Filter.atTop (𝓝 (f OnePoint.infty))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NoncompactSpace X<GOAL>DenseRange OnePoint.some
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>NoncompactSpace X<GOAL>DenseEmbedding OnePoint.some
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>↑x ⤳ ↑y ↔ x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>Inseparable ↑x ↑y ↔ Inseparable x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>¬OnePoint.infty ⤳ ↑x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>¬Inseparable OnePoint.infty ↑x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>¬Inseparable (↑x) OnePoint.infty
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : OnePoint X<GOAL>Inseparable x y ↔ x = OnePoint.infty ∧ y = OnePoint.infty ∨ ∃ x', x = ↑x' ∧ ∃ y', y = ↑y' ∧ Inseparable x' y'
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>Infinite X<VAR>DiscreteTopology X<GOAL>¬Continuous ⇑CofiniteTopology.of.symm
<GOAL>∃ α β x x_1, CompactSpace α ∧ T1Space β ∧ ∃ f, Continuous ⇑f ∧ ¬Continuous ⇑f.symm
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>TopologicalSpace Y<VAR>X : Cᵒᵖ<GOAL>(ContinuousMap.yonedaPresheaf F Y).obj X = C(↑(F.obj (Opposite.unop X)), Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>TopologicalSpace Y<GOAL>∀ {X Y_1 : Cᵒᵖ} (f : X ⟶ Y_1) (g : C(↑(F.obj (Opposite.unop X)), Y)), (ContinuousMap.yonedaPresheaf F Y).map f g = g.comp (F.map f.unop)
<VAR>Y : Type w'<VAR>TopologicalSpace Y<VAR>X : TopCatᵒᵖ<GOAL>(ContinuousMap.yonedaPresheaf' Y).obj X = C(↑(Opposite.unop X), Y)
<VAR>Y : Type w'<VAR>TopologicalSpace Y<GOAL>∀ {X Y_1 : TopCatᵒᵖ} (f : X ⟶ Y_1) (g : C(↑(Opposite.unop X), Y)), (ContinuousMap.yonedaPresheaf' Y).map f g = g.comp f.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : C ⥤ TopCat<VAR>Y : Type w'<VAR>TopologicalSpace Y<GOAL>ContinuousMap.yonedaPresheaf F Y = F.op ⋙ ContinuousMap.yonedaPresheaf' Y
<VAR>Y : Type w'<VAR>TopologicalSpace Y<VAR>α : Type<VAR>X : α → TopCat<GOAL>(CategoryTheory.Limits.piComparison (ContinuousMap.yonedaPresheaf' Y) fun x => Opposite.op (X x)) = (ContinuousMap.yonedaPresheaf' Y).map ((CategoryTheory.Limits.opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫ (equivEquivIso (ContinuousMap.sigmaEquiv Y fun x => ↑(X x))).inv ≫ (CategoryTheory.Limits.Types.productIso fun i => C(↑(X i), Y)).inv
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<GOAL>ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a x : 𝕜<GOAL>ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a : 𝕜<VAR>x : 𝕜<VAR>hx : ↑x ≠ ↑a<GOAL>toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a : 𝕜<VAR>x : 𝕜<VAR>hx : ↑x ≠ ↑a<GOAL>ContinuousAt (toIcoMod hp a) x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>Archimedean 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>a : 𝕜<VAR>x : 𝕜<VAR>hx : ↑x ≠ ↑a<GOAL>ContinuousAt (toIocMod hp a) x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p : 𝕜<VAR>n : ℕ<VAR>x : 𝕜<GOAL>↑(n • x) = n • ↑x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p : 𝕜<VAR>n : ℤ<VAR>x : 𝕜<GOAL>↑(n • x) = n • ↑x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p x y : 𝕜<GOAL>↑(x + y) = ↑x + ↑y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p x y : 𝕜<GOAL>↑(x - y) = ↑x - ↑y
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p : 𝕜<VAR>x : 𝕜<GOAL>↑(-x) = -↑x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p : 𝕜<VAR>x : 𝕜<GOAL>↑x = 0 ↔ ∃ n, n • p = x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>↑x = 0 ↔ ∃ n, n • p = x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p : 𝕜<GOAL>↑p = 0
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>p x : 𝕜<GOAL>↑(x + p) = ↑x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>p : 𝕜<GOAL>Continuous ⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>x y : 𝕜<VAR>hx : x ∈ Set.Ico a (a + p)<VAR>hy : y ∈ Set.Ico a (a + p)<GOAL>↑x = ↑y ↔ x = y
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Set.Ico a (a + p)<GOAL>AddCircle.liftIco p a f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Set.Ioc a (a + p)<GOAL>AddCircle.liftIoc p a f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<VAR>a : AddCircle p<GOAL>∃ b ∈ Set.Ico 0 p, ↑b = a
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>ha : a ∈ Set.Ico 0 p<GOAL>↑a = 0 ↔ a = 0
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<GOAL>Continuous ⇑(AddCircle.equivIco p a).symm
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<GOAL>Continuous ⇑(AddCircle.equivIoc p a).symm
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a<GOAL>ContinuousAt (⇑(AddCircle.equivIco p a)) x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a<GOAL>ContinuousAt (⇑(AddCircle.equivIoc p a)) x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>DiscreteTopology ↥(AddSubgroup.zmultiples p)<GOAL>(AddCircle.partialHomeomorphCoe p a).target = {↑a}ᶜ
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>DiscreteTopology ↥(AddSubgroup.zmultiples p)<VAR>x : AddCircle p<GOAL>↑(AddCircle.partialHomeomorphCoe p a).symm x = ↑((AddCircle.equivIco p a) x)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>DiscreteTopology ↥(AddSubgroup.zmultiples p)<GOAL>(AddCircle.partialHomeomorphCoe p a).source = Set.Ioo a (a + p)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<VAR>DiscreteTopology ↥(AddSubgroup.zmultiples p)<GOAL>∀ (a_1 : 𝕜), ↑(AddCircle.partialHomeomorphCoe p a) a_1 = ↑a_1
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<VAR>DiscreteTopology ↥(AddSubgroup.zmultiples p)<VAR>DenselyOrdered 𝕜<GOAL>IsLocalHomeomorph QuotientAddGroup.mk
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<GOAL>QuotientAddGroup.mk '' Set.Ico a (a + p) = Set.univ
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<GOAL>QuotientAddGroup.mk '' Set.Ioc a (a + p) = Set.univ
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>Archimedean 𝕜<GOAL>QuotientAddGroup.mk '' Set.Icc a (a + p) = Set.univ
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>x : 𝕜<GOAL>(AddCircle.equivAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>x : 𝕜<GOAL>(AddCircle.equivAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>x : 𝕜<GOAL>(AddCircle.homeomorphAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : p ≠ 0<VAR>hq : q ≠ 0<VAR>x : 𝕜<GOAL>(AddCircle.homeomorphAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>FloorRing 𝕜<VAR>x : 𝕜<GOAL>↑((AddCircle.equivIco p 0) ↑x) = Int.fract (x / p) * p
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>h : 0 < n<GOAL>addOrderOf ↑(p / ↑n) = n
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>m : ℕ<VAR>hn : 0 < n<GOAL>m.gcd n * addOrderOf ↑(↑m / ↑n * p) = n
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>m n : ℕ<VAR>hn : 0 < n<VAR>h : m.gcd n = 1<GOAL>addOrderOf ↑(↑m / ↑n * p) = n
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : m.natAbs.gcd n = 1<GOAL>addOrderOf ↑(↑m / ↑n * p) = n
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>q : ℚ<GOAL>addOrderOf ↑(↑q * p) = q.den
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>h : 0 < n<GOAL>addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>h : IsOfFinAddOrder u<GOAL>∃ m, m.gcd (addOrderOf u) = 1 ∧ m < addOrderOf u ∧ ↑(↑m / ↑(addOrderOf u) * p) = u
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<GOAL>Nat.card { u // addOrderOf u = n } = n.totient
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>{u | addOrderOf u = n}.Finite
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<GOAL>⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (AddCircle.EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<GOAL>⇑(AddCircle.equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (AddCircle.EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>h : f a = f (a + p)<GOAL>AddCircle.liftIco p a f = Quot.lift ((Set.Icc a (a + p)).restrict f) ⋯ ∘ ⇑(AddCircle.equivIccQuot p a)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p a : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<VAR>TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f a = f (a + p)<VAR>hc : ContinuousOn f (Set.Icc a (a + p))<GOAL>Continuous (AddCircle.liftIco p a f)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<VAR>f : 𝕜 → B<VAR>x : 𝕜<VAR>hx : x ∈ Set.Ico 0 p<GOAL>AddCircle.liftIco p 0 f ↑x = f x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>LinearOrderedAddCommGroup 𝕜<VAR>TopologicalSpace 𝕜<VAR>OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>Archimedean 𝕜<VAR>TopologicalSpace B<VAR>f : 𝕜 → B<VAR>hf : f 0 = f p<VAR>hc : ContinuousOn f (Set.Icc 0 p)<GOAL>Continuous (AddCircle.liftIco p 0 f)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ℤ<GOAL>ZMod.toAddCircle ↑j = ↑(↑j / ↑N)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ℕ<GOAL>ZMod.toAddCircle ↑j = ↑(↑j / ↑N)
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ZMod N<GOAL>ZMod.toAddCircle j = ↑(↑j.val / ↑N)
<VAR>N : ℕ<VAR>NeZero N<GOAL>Function.Injective ⇑ZMod.toAddCircle
<VAR>N : ℕ<VAR>NeZero N<VAR>j k : ZMod N<GOAL>ZMod.toAddCircle j = ZMod.toAddCircle k ↔ j = k
<VAR>N : ℕ<VAR>NeZero N<VAR>j : ZMod N<GOAL>ZMod.toAddCircle j = 0 ↔ j = 0
<GOAL>TopCat.adj₁.unit = { app := fun X => id, naturality := TopCat.adj₁.proof_1 }
<GOAL>TopCat.adj₁.counit = { app := fun X => { toFun := id, continuous_toFun := ⋯ }, naturality := TopCat.adj₁.proof_3 }
<GOAL>TopCat.adj₂.counit = { app := fun X => id, naturality := TopCat.adj₂.proof_3 }
<GOAL>TopCat.adj₂.unit = { app := fun X => { toFun := id, continuous_toFun := ⋯ }, naturality := TopCat.adj₂.proof_2 }
<VAR>self : Sequential<GOAL>SequentialSpace ↑self.toTop
<VAR>self : Sequential<GOAL>Sequential.sequentialToTop.obj self = self.toTop
<GOAL>∀ {X Y : CategoryTheory.InducedCategory TopCat Sequential.toTop} (f : X ⟶ Y), Sequential.sequentialToTop.map f = f
<VAR>X Y : Sequential<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>(Sequential.isoOfHomeo f).inv = { toFun := ⇑f.symm, continuous_toFun := ⋯ }
<VAR>X Y : Sequential<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>(Sequential.isoOfHomeo f).hom = { toFun := ⇑f, continuous_toFun := ⋯ }
<VAR>X Y : Sequential<VAR>f : X ≅ Y<VAR>a : (CategoryTheory.forget Sequential).obj Y<GOAL>(Sequential.homeoOfIso f).symm a = f.inv a
<VAR>X Y : Sequential<VAR>f : X ≅ Y<VAR>a : (CategoryTheory.forget Sequential).obj X<GOAL>(Sequential.homeoOfIso f) a = f.hom a
<VAR>X Y : Sequential<VAR>f : X ≅ Y<GOAL>Sequential.isoEquivHomeo f = Sequential.homeoOfIso f
<VAR>X Y : Sequential<VAR>f : ↑X.toTop ≃ₜ ↑Y.toTop<GOAL>Sequential.isoEquivHomeo.symm f = Sequential.isoOfHomeo f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>f.NeBot<VAR>hf : f ≤ 𝓟 s<GOAL>∃ x ∈ s, ClusterPt x f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type u_2<VAR>hs : IsCompact s<VAR>f : Filter ι<VAR>f.NeBot<VAR>u : ι → X<VAR>hf : Filter.map u f ≤ 𝓟 s<GOAL>∃ x ∈ s, MapClusterPt x f u
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>f : Filter X<VAR>hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>p : Set X → Prop<VAR>he : p ∅<VAR>hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s<VAR>hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)<VAR>hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t<GOAL>p s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<GOAL>IsCompact (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>ht : IsCompact t<VAR>hs : IsClosed s<GOAL>IsCompact (s ∩ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsOpen t<GOAL>IsCompact (s \ t)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>h : t ⊆ s<GOAL>IsCompact t
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f : X → Y<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<GOAL>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>hs : IsCompact s<VAR>hf : Continuous f<GOAL>IsCompact (f '' s)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s t : Set X<VAR>f : Filter X<VAR>hs : IsCompact s<VAR>hf₂ : f ≤ 𝓟 s<VAR>ht₁ : IsOpen t<VAR>ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t<GOAL>t ∈ f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>l : Filter X<VAR>y : X<VAR>hmem : s ∈ l<VAR>h : ∀ x ∈ s, ClusterPt x l → x = y<GOAL>l ≤ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>s : Set X<VAR>l : Filter Y<VAR>y : X<VAR>f : Y → X<VAR>hs : IsCompact s<VAR>hmem : ∀ᶠ (x : Y) in l, f x ∈ s<VAR>h : ∀ x ∈ s, MapClusterPt x l f → x = y<GOAL>Filter.Tendsto f l (𝓝 y)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<VAR>hdU : Directed (fun x x_1 => x ⊆ x_1) U<GOAL>∃ i, s ⊆ U i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hs : IsCompact s<VAR>U : ι → Set X<VAR>hUo : ∀ (i : ι), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ t, s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<GOAL>∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ 𝓝ˢ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<GOAL>∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : (x : X) → x ∈ s → Set X<VAR>hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x<GOAL>∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>U : X → Set X<VAR>hU : ∀ x ∈ s, U x ∈ 𝓝 x<GOAL>∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<GOAL>Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>l : Filter X<VAR>hs : IsCompact s<GOAL>Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<VAR>hdt : Directed (fun x x_1 => x ⊇ x_1) t<GOAL>∃ i, s ∩ t i = ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<GOAL>∃ u, s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>f : ι → Set X<VAR>hf : LocallyFinite f<VAR>hs : IsCompact s<GOAL>{i | (f i ∩ s).Nonempty}.Finite
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>ι : Type v<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty<GOAL>(s ∩ ⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>ι : Type v<VAR>hι : Nonempty ι<VAR>t : ι → Set X<VAR>htd : Directed (fun x x_1 => x ⊇ x_1) t<VAR>htn : ∀ (i : ι), (t i).Nonempty<VAR>htc : ∀ (i : ι), IsCompact (t i)<VAR>htcl : ∀ (i : ι), IsClosed (t i)<GOAL>(⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : Nonempty ↑S<VAR>hSd : DirectedOn (fun x x_1 => x ⊇ x_1) S<VAR>hSn : ∀ U ∈ S, U.Nonempty<VAR>hSc : ∀ U ∈ S, IsCompact U<VAR>hScl : ∀ U ∈ S, IsClosed U<GOAL>(⋂₀ S).Nonempty
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>t : ℕ → Set X<VAR>htd : ∀ (i : ℕ), t (i + 1) ⊆ t i<VAR>htn : ∀ (i : ℕ), (t i).Nonempty<VAR>ht0 : IsCompact (t 0)<VAR>htcl : ∀ (i : ℕ), IsClosed (t i)<GOAL>(⋂ i, t i).Nonempty
<VAR>X : Type u<VAR>ι : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>b : Set ι<VAR>c : ι → Set X<VAR>hs : IsCompact s<VAR>hc₁ : ∀ i ∈ b, IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i ∈ b, c i<GOAL>∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i<GOAL>IsCompact s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅<GOAL>IsCompact s
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsCompact s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>IsCompact s ↔ ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>K : Set X<VAR>l : Filter Y<VAR>s : Set (X × Y)<VAR>hK : IsCompact K<VAR>hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l<GOAL>s ∈ 𝓝ˢ K ×ˢ l
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>l : Filter Y<GOAL>𝓝ˢ K ×ˢ l = ⨆ x ∈ K, 𝓝 x ×ˢ l
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>l : Filter X<GOAL>l ×ˢ 𝓝ˢ K = ⨆ y ∈ K, l ×ˢ 𝓝 y
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace Y<VAR>K : Set Y<VAR>l : Filter X<VAR>s : Set (X × Y)<VAR>hK : IsCompact K<VAR>hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y<GOAL>s ∈ l ×ˢ 𝓝ˢ K
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>l : Filter X<GOAL>𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>l : Filter X<GOAL>l ⊓ 𝓝ˢ K = ⨆ x ∈ K, l ⊓ 𝓝 x
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>K : Set X<VAR>l : Filter X<VAR>s : Set X<VAR>hK : IsCompact K<VAR>hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l<GOAL>s ∈ 𝓝ˢ K ⊓ l
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>K : Set X<VAR>l : Filter X<VAR>s : Set X<VAR>hK : IsCompact K<VAR>hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y<GOAL>s ∈ l ⊓ 𝓝ˢ K
<VAR>X : Type u<VAR>Y : Type v<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₀ : X<VAR>K : Set Y<VAR>hK : IsCompact K<VAR>P : X → Y → Prop<VAR>hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2<GOAL>∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>IsCompact ∅
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : X<GOAL>IsCompact {x}
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : s.Subsingleton<GOAL>IsCompact s