ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a : α<VAR>(𝓝[<] a).NeBot<GOAL>(𝓝ˢ (Set.Ici a)).HasBasis (fun x => x < a) Set.Ici
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a b : α<VAR>(𝓝[<] b).NeBot<GOAL>Set.Ici a ∈ 𝓝ˢ (Set.Ici b) ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : f '' s ∈ 𝓝[≥] f a<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≥] f a<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : f '' s ∈ 𝓝[≥] f a<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : Set.SurjOn f s (Set.Ioi (f a))<GOAL>ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≤] f a<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : f '' s ∈ 𝓝[≤] f a<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : closure (f '' s) ∈ 𝓝[≤] f a<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : f '' s ∈ 𝓝[≤] f a<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≤] a<VAR>hfs : Set.SurjOn f s (Set.Iio (f a))<GOAL>ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝 a<VAR>hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)<VAR>hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b<GOAL>ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝 a<VAR>hfs : closure (f '' s) ∈ 𝓝 (f a)<GOAL>ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝 a<VAR>hfs : f '' s ∈ 𝓝 (f a)<GOAL>ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝 a<VAR>hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)<VAR>hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b<GOAL>ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝 a<VAR>hfs : closure (f '' s) ∈ 𝓝 (f a)<GOAL>ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : MonotoneOn f s<VAR>hs : s ∈ 𝓝 a<VAR>hfs : f '' s ∈ 𝓝 (f a)<GOAL>ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_dense : DenseRange f<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>LinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>DenselyOrdered β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>h_surj : Function.Surjective f<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>OrderTopology α<VAR>OrderTopology β<VAR>e : α ≃o β<GOAL>Continuous ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>OrderTopology α<VAR>OrderTopology β<VAR>e : α ≃o β<GOAL>⇑e.toHomeomorph = ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>OrderTopology α<VAR>OrderTopology β<VAR>e : α ≃o β<GOAL>⇑e.toHomeomorph.symm = ⇑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>f : γ → ↑(Set.Icc a b) → β<VAR>la : Filter α<VAR>lb : Filter β<VAR>lc : Filter γ<VAR>hf : Filter.Tendsto (↿f) (lc ×ˢ Filter.map (Set.projIcc a b h) la) lb<GOAL>Filter.Tendsto (↿(Set.IccExtend h ∘ f)) (lc ×ˢ la) lb
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>Continuous (Set.projIcc a b h)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>QuotientMap (Set.projIcc a b h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>f : ↑(Set.Icc a b) → β<GOAL>Continuous (Set.IccExtend h f) ↔ Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace γ<VAR>a b : α<VAR>h : a ≤ b<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>f : γ → ↑(Set.Icc a b) → β<VAR>g : γ → α<VAR>hf : Continuous ↿f<VAR>hg : Continuous g<GOAL>Continuous fun a_1 => Set.IccExtend h (f a_1) (g a_1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>f : ↑(Set.Icc a b) → β<VAR>hf : Continuous f<GOAL>Continuous (Set.IccExtend h f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace γ<VAR>a b : α<VAR>h : a ≤ b<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>x : γ<VAR>f : γ → ↑(Set.Icc a b) → β<VAR>g : γ → α<VAR>hf : ContinuousAt (↿f) (x, Set.projIcc a b h (g x))<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun a_1 => Set.IccExtend h (f a_1) (g a_1)) x
<VAR>α : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : PriestleySpace α<VAR>x y : α<GOAL>¬x ≤ y → ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>PriestleySpace α<VAR>x y : α<GOAL>¬x ≤ y → ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>PriestleySpace α<VAR>x y : α<VAR>h : ¬x ≤ y<GOAL>∃ U, IsClopen U ∧ IsLowerSet U ∧ x ∉ U ∧ y ∈ U
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>PriestleySpace α<VAR>x y : α<VAR>h : x ≠ y<GOAL>∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Bornology α<VAR>Bornology β<VAR>self : LocallyBoundedMap α β<GOAL>Filter.comap self.toFun (Bornology.cobounded β) ≤ Bornology.cobounded α
<VAR>F : Type u_6<VAR>α : outParam (Type u_7)<VAR>β : outParam (Type u_8)<VAR>Bornology α<VAR>Bornology β<VAR>FunLike F α β<VAR>self : LocallyBoundedMapClass F α β<VAR>f : F<GOAL>Filter.comap (⇑f) (Bornology.cobounded β) ≤ Bornology.cobounded α
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>Bornology α<VAR>Bornology β<VAR>LocallyBoundedMapClass F α β<VAR>f : F<VAR>s : Set α<VAR>hs : Bornology.IsBounded s<GOAL>Bornology.IsBounded (⇑f '' s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f g : LocallyBoundedMap α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f : LocallyBoundedMap α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f : LocallyBoundedMap α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f : α → β<VAR>h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)<GOAL>⇑(LocallyBoundedMap.ofMapBounded f h) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f : α → β<VAR>h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)<VAR>a : α<GOAL>(LocallyBoundedMap.ofMapBounded f h) a = f a
<VAR>α : Type u_2<VAR>Bornology α<GOAL>⇑(LocallyBoundedMap.id α) = id
<VAR>α : Type u_2<VAR>Bornology α<VAR>a : α<GOAL>(LocallyBoundedMap.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bornology α<VAR>Bornology β<VAR>Bornology γ<VAR>f : LocallyBoundedMap β γ<VAR>g : LocallyBoundedMap α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bornology α<VAR>Bornology β<VAR>Bornology γ<VAR>f : LocallyBoundedMap β γ<VAR>g : LocallyBoundedMap α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>Bornology α<VAR>Bornology β<VAR>Bornology γ<VAR>Bornology δ<VAR>f : LocallyBoundedMap γ δ<VAR>g : LocallyBoundedMap β γ<VAR>h : LocallyBoundedMap α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f : LocallyBoundedMap α β<GOAL>f.comp (LocallyBoundedMap.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>Bornology β<VAR>f : LocallyBoundedMap α β<GOAL>(LocallyBoundedMap.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bornology α<VAR>Bornology β<VAR>Bornology γ<VAR>g₁ g₂ : LocallyBoundedMap β γ<VAR>f : LocallyBoundedMap α β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>Bornology α<VAR>Bornology β<VAR>Bornology γ<VAR>g : LocallyBoundedMap β γ<VAR>f₁ f₂ : LocallyBoundedMap α β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>t : Set X<VAR>hS : RestrictGenTopology S<GOAL>IsOpen t ↔ ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>t : Set X<VAR>hS : RestrictGenTopology S<GOAL>IsClosed t ↔ ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hS : RestrictGenTopology S<GOAL>Continuous f ↔ ∀ s ∈ S, ContinuousOn f s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous f<GOAL>RestrictGenTopology S
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>h : ∀ (t : Set X), (∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)) → IsClosed t<GOAL>RestrictGenTopology S
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S T : Set (Set X)<VAR>hS : RestrictGenTopology S<VAR>hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t<GOAL>RestrictGenTopology T
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S T : Set (Set X)<VAR>hS : RestrictGenTopology S<VAR>hT : S ⊆ T<GOAL>RestrictGenTopology T
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>SequentialSpace X<VAR>h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Filter.Tendsto u Filter.atTop (𝓝 x) → insert x (Set.range u) ∈ S<GOAL>RestrictGenTopology S
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>SequentialSpace X<GOAL>RestrictGenTopology {K | IsCompact K}
<VAR>L : Type u_1<VAR>CompleteLattice L<VAR>u : L<GOAL>(Locale.openOfElementHom L) u = {x | x u}
<VAR>L : Type u_1<VAR>CompleteLattice L<VAR>U : Set (Locale.PT L)<GOAL>IsOpen U ↔ ∃ u, {x | x u} = U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>∀ (x_1 : TopologicalSpace.Opens X), (Locale.localePointOfSpacePoint X x) x_1 = (x ∈ x_1)
<VAR>X : Type u_1<VAR>LinearOrder X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>a : X<VAR>s : Set X<GOAL>s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a
<VAR>X : Type u_1<VAR>LinearOrder X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>a : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
<VAR>X : Type u_1<VAR>LinearOrder X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>a : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a
<VAR>X : Type u_1<VAR>LinearOrder X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>a : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a
<VAR>X : Type u_1<VAR>LinearOrder X<VAR>TopologicalSpace X<VAR>OrderTopology X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<GOAL>s.ordT5Nhd t ∈ 𝓝ˢ s
<VAR>α : Type u_4<VAR>self : Bornology α<GOAL>Bornology.cobounded' ≤ Filter.cofinite
<VAR>α : Type u_4<VAR>Bornology α<GOAL>Bornology.cobounded α ≤ Filter.cofinite
<VAR>α : Type u_2<VAR>t t' : Bornology α<VAR>h_cobounded : Bornology.cobounded α = Bornology.cobounded α<GOAL>t = t'
<VAR>α : Type u_2<VAR>t t' : Bornology α<GOAL>t = t' ↔ Bornology.cobounded α = Bornology.cobounded α
<VAR>α : Type u_4<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>singleton_mem : ∀ (x : α), {x} ∈ B<GOAL>Bornology.cobounded α = Filter.comk (fun x => x ∈ B) empty_mem subset_mem union_mem
<VAR>α : Type u_4<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ⋃₀ B = Set.univ<GOAL>Bornology.cobounded α = Filter.comk (fun x => x ∈ B) empty_mem subset_mem union_mem
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, Bornology.IsCobounded s ↔ s ∈ Bornology.cobounded α
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, Bornology.IsBounded s ↔ sᶜ ∈ Bornology.cobounded α
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, Bornology.IsBounded sᶜ ↔ Bornology.IsCobounded s
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, Bornology.IsCobounded sᶜ ↔ Bornology.IsBounded s
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α}, Bornology.IsBounded ∅
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, ¬Bornology.IsBounded s → s.Nonempty
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {x_1 : α}, Bornology.IsBounded {x_1}
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, Bornology.IsBounded s ↔ ∀ x_1 ∈ s, Bornology.IsBounded s
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α}, Bornology.IsCobounded Set.univ
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s t : Set α}, Bornology.IsCobounded (s ∩ t) ↔ Bornology.IsCobounded s ∧ Bornology.IsCobounded t
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s t : Set α}, Bornology.IsCobounded s → Bornology.IsCobounded t → Bornology.IsCobounded (s ∩ t)
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s t : Set α}, Bornology.IsBounded (s ∪ t) ↔ Bornology.IsBounded s ∧ Bornology.IsBounded t
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s t : Set α}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s ∪ t)
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s t : Set α}, Bornology.IsCobounded s → s ⊆ t → Bornology.IsCobounded t
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s t : Set α}, Bornology.IsBounded t → s ⊆ t → Bornology.IsBounded s
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α}, ⋃₀ {s | Bornology.IsBounded s} = Set.univ
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α}, Bornology.IsBounded s → ∀ (x_1 : α), Bornology.IsBounded (insert x_1 s)
<VAR>α : Type u_2<GOAL>∀ {x : Bornology α} {s : Set α} {x_1 : α}, Bornology.IsBounded (insert x_1 s) ↔ Bornology.IsBounded s
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>∀ {x : Bornology α} [inst : Bornology β] {f : α → β}, Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α ↔ ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)
<VAR>α : Type u_2<VAR>t t' : Bornology α<GOAL>t = t' ↔ ∀ (s : Set α), s ∈ Bornology.cobounded α ↔ s ∈ Bornology.cobounded α
<VAR>α : Type u_2<VAR>t t' : Bornology α<GOAL>t = t' ↔ ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
<VAR>α : Type u_2<VAR>s : Set α<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ∀ (x : α), {x} ∈ B<GOAL>Bornology.IsCobounded s ↔ sᶜ ∈ B
<VAR>α : Type u_2<VAR>s : Set α<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ∀ (x : α), {x} ∈ B<GOAL>Bornology.IsBounded s ↔ s ∈ B
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set ι<VAR>f : ι → Set α<VAR>hs : s.Finite<GOAL>Bornology.IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsCobounded (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>Bornology.IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsCobounded (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Bornology α<VAR>Finite ι<VAR>f : ι → Set α<GOAL>Bornology.IsCobounded (⋂ i, f i) ↔ ∀ (i : ι), Bornology.IsCobounded (f i)
<VAR>α : Type u_2<VAR>Bornology α<VAR>S : Set (Set α)<VAR>hs : S.Finite<GOAL>Bornology.IsCobounded (⋂₀ S) ↔ ∀ s ∈ S, Bornology.IsCobounded s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set ι<VAR>f : ι → Set α<VAR>hs : s.Finite<GOAL>Bornology.IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsBounded (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>Bornology.IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsBounded (f i)
<VAR>α : Type u_2<VAR>Bornology α<VAR>S : Set (Set α)<VAR>hs : S.Finite<GOAL>Bornology.IsBounded (⋃₀ S) ↔ ∀ s ∈ S, Bornology.IsBounded s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Bornology α<VAR>Finite ι<VAR>s : ι → Set α<GOAL>Bornology.IsBounded (⋃ i, s i) ↔ ∀ (i : ι), Bornology.IsBounded (s i)
<VAR>α : Type u_2<VAR>Bornology α<VAR>a : α<GOAL>∀ᶠ (x : α) in Bornology.cobounded α, x ≠ a
<VAR>α : Type u_2<VAR>Bornology α<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>l : Filter α<VAR>h : l.HasBasis p s<GOAL>Disjoint l (Bornology.cobounded α) ↔ ∃ i, p i ∧ Bornology.IsBounded (s i)
<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>Bornology.IsBounded s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Bornology α<VAR>f : β → α<VAR>l : Filter β<VAR>h : Filter.Tendsto f l (Bornology.cobounded α)<VAR>a : α<GOAL>∀ᶠ (x : β) in l, f x ≠ a
<VAR>α : Type u_4<VAR>Bornology α<VAR>self : BoundedSpace α<GOAL>Bornology.IsBounded Set.univ
<VAR>α : Type u_2<VAR>Bornology α<GOAL>Bornology.IsBounded Set.univ ↔ BoundedSpace α
<VAR>α : Type u_2<VAR>Bornology α<GOAL>Bornology.cobounded α = ⊥ ↔ BoundedSpace α
<VAR>α : Type u_2<VAR>Bornology α<VAR>BoundedSpace α<VAR>s : Set α<GOAL>Bornology.IsBounded s
<VAR>α : Type u_2<VAR>Bornology α<VAR>BoundedSpace α<VAR>s : Set α<GOAL>Bornology.IsCobounded s
<VAR>α : Type u_2<VAR>Bornology α<VAR>BoundedSpace α<GOAL>Bornology.cobounded α = ⊥
<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set α<GOAL>Bornology.IsCobounded (⇑OrderDual.ofDual ⁻¹' s) ↔ Bornology.IsCobounded s
<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set αᵒᵈ<GOAL>Bornology.IsCobounded (⇑OrderDual.toDual ⁻¹' s) ↔ Bornology.IsCobounded s
<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set α<GOAL>Bornology.IsBounded (⇑OrderDual.ofDual ⁻¹' s) ↔ Bornology.IsBounded s
<VAR>α : Type u_2<VAR>Bornology α<VAR>s : Set αᵒᵈ<GOAL>Bornology.IsBounded (⇑OrderDual.toDual ⁻¹' s) ↔ Bornology.IsBounded s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<GOAL>Bornology.cobounded (α × β) = (Bornology.cobounded α).coprod (Bornology.cobounded β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set (α × β)<GOAL>Bornology.IsBounded (Prod.fst '' s) ∧ Bornology.IsBounded (Prod.snd '' s) ↔ Bornology.IsBounded s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set (α × β)<VAR>hs : Bornology.IsBounded s<GOAL>Bornology.IsBounded (Prod.fst '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set (α × β)<VAR>hs : Bornology.IsBounded s<GOAL>Bornology.IsBounded (Prod.snd '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set α<VAR>t : Set β<VAR>h : Bornology.IsBounded (s ×ˢ t)<VAR>ht : t.Nonempty<GOAL>Bornology.IsBounded s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set α<VAR>t : Set β<VAR>h : Bornology.IsBounded (s ×ˢ t)<VAR>hs : s.Nonempty<GOAL>Bornology.IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set α<VAR>t : Set β<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<GOAL>Bornology.IsBounded (s ×ˢ t)