ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<GOAL>GaloisConnection exterior interior
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>s : Set α<GOAL>exterior (exterior s) = exterior s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>s t : Set α<GOAL>exterior (s ∪ t) = exterior s ∪ exterior t
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>s : Set α<GOAL>𝓝ˢ (exterior s) = 𝓝ˢ s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>s : Set α<GOAL>𝓟 (exterior s) = 𝓝ˢ s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>AlexandrovDiscrete α<GOAL>exterior s ⊆ exterior t ↔ 𝓝ˢ s ≤ 𝓝ˢ t
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>x y : α<VAR>AlexandrovDiscrete α<GOAL>x ⤳ y ↔ exterior {x} ⊆ exterior {y}
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>AlexandrovDiscrete α<GOAL>IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>IsCompact (exterior s)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AlexandrovDiscrete α<VAR>f : β → α<VAR>h : Inducing f<GOAL>AlexandrovDiscrete β
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<VAR>β : Type u_5<VAR>f : α → β<GOAL>AlexandrovDiscrete β
<VAR>α : Type u_3<VAR>t₁ t₂ : TopologicalSpace α<GOAL>AlexandrovDiscrete α → AlexandrovDiscrete α → AlexandrovDiscrete α
<VAR>ι : Sort u_1<VAR>α : Type u_3<VAR>t : ι → TopologicalSpace α<GOAL>(∀ (i : ι), AlexandrovDiscrete α) → AlexandrovDiscrete α
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>x : X<GOAL>𝓝 x = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : CompactSpace X<GOAL>IsCompact Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>self : NoncompactSpace X<GOAL>¬IsCompact Set.univ
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>self : WeaklyLocallyCompactSpace X<VAR>x : X<GOAL>∃ s, IsCompact s ∧ s ∈ 𝓝 x
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>self : LocallyCompactSpace X<VAR>x : X<VAR>n : Set X<GOAL>n ∈ 𝓝 x → ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>self : LocallyCompactPair X Y<VAR>f : X → Y<VAR>x : X<VAR>s : Set Y<GOAL>Continuous f → s ∈ 𝓝 (f x) → ∃ K ∈ 𝓝 x, IsCompact K ∧ Set.MapsTo f K s
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>PartialOrder X<VAR>OrderTopology X<VAR>NoMaxOrder X<GOAL>Filter.Tendsto 𝓝 Filter.atTop (𝓝 Filter.atTop)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>PartialOrder X<VAR>OrderTopology X<VAR>NoMinOrder X<GOAL>Filter.Tendsto 𝓝 Filter.atBot (𝓝 Filter.atBot)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>PartialOrder X<VAR>OrderTopology X<VAR>NoMaxOrder X<VAR>f : α → X<VAR>l : Filter α<VAR>h : Filter.Tendsto f l Filter.atTop<GOAL>Filter.Tendsto (𝓝 ∘ f) l (𝓝 Filter.atTop)
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>PartialOrder X<VAR>OrderTopology X<VAR>NoMinOrder X<VAR>f : α → X<VAR>l : Filter α<VAR>h : Filter.Tendsto f l Filter.atBot<GOAL>Filter.Tendsto (𝓝 ∘ f) l (𝓝 Filter.atBot)
<VAR>ι : Type u_1<VAR>F : Filter ι<VAR>f : ι → ℝ<VAR>h : Bornology.IsBounded (Set.range f)<GOAL>Filter.IsBounded (fun x x_1 => x ≤ x_1) (Filter.map f F)
<VAR>ι : Type u_1<VAR>F : Filter ι<VAR>f : ι → ℝ<VAR>h : Bornology.IsBounded (Set.range f)<GOAL>Filter.IsBounded (fun x x_1 => x ≥ x_1) (Filter.map f F)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<VAR>(𝓝[<] a).NeBot<GOAL>∃ᶠ (x : α) in 𝓝 a, x < a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<VAR>(𝓝[>] a).NeBot<GOAL>∃ᶠ (x : α) in 𝓝 a, a < x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<VAR>(𝓝[<] a).NeBot<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in 𝓝 a, p x<GOAL>∃ b < a, p b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<VAR>(𝓝[>] a).NeBot<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in 𝓝 a, p x<GOAL>∃ b > a, p b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a b : α<VAR>H₂ : a ≤ b<GOAL>(𝓝[Set.Ici a] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a b : α<VAR>H : a ≤ b<GOAL>(𝓝[Set.Iic b] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<GOAL>𝓝[<] a ≤ 𝓝[≠] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<GOAL>𝓝[>] a ≤ 𝓝[≠] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>∀ (x : α), (𝓝[<] x).NeBot<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>interior s = ∅
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>∀ (x : α), (𝓝[>] x).NeBot<VAR>s : Set α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>interior s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousWithinAt f (Set.Ioi a) a ↔ ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousWithinAt f (Set.Iio a) a ↔ ContinuousWithinAt f (Set.Iic a) a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>a : α<GOAL>𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>a : α<GOAL>𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>a : α<GOAL>𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>a : α<GOAL>𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>a : α<GOAL>𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iic a) a ∧ ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>TopologicalSpace β<VAR>a : α<VAR>f : α → β<GOAL>ContinuousAt f a ↔ ContinuousWithinAt f (Set.Iio a) a ∧ ContinuousWithinAt f (Set.Ioi a) a
<VAR>α : Type u_1<VAR>s : Set α<VAR>Lattice α<VAR>Nonempty α<GOAL>Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
<VAR>α : Type u_1<VAR>Bornology α<VAR>Preorder α<VAR>self : IsOrderBornology α<VAR>s : Set α<GOAL>Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
<VAR>α : Type u_1<VAR>Bornology α<VAR>Lattice α<VAR>Nonempty α<GOAL>IsOrderBornology α ↔ inst✝ = orderBornology
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<VAR>Preorder α<VAR>IsOrderBornology α<GOAL>Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<VAR>Preorder α<VAR>IsOrderBornology α<VAR>hs : Bornology.IsBounded s<GOAL>BddBelow s
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<VAR>Preorder α<VAR>IsOrderBornology α<VAR>hs : Bornology.IsBounded s<GOAL>BddAbove s
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<VAR>Preorder α<VAR>IsOrderBornology α<VAR>hs₀ : BddBelow s<VAR>hs₁ : BddAbove s<GOAL>Bornology.IsBounded s
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<VAR>Preorder α<VAR>IsOrderBornology α<VAR>hs₀ : BddAbove s<VAR>hs₁ : BddBelow s<GOAL>Bornology.IsBounded s
<VAR>α : Type u_1<VAR>Bornology α<VAR>s t : Set α<VAR>Preorder α<VAR>IsOrderBornology α<VAR>hs : BddBelow s<VAR>ht : BddAbove t<GOAL>Bornology.IsBounded (s ∩ t)
<VAR>α : Type u_1<VAR>Bornology α<VAR>s t : Set α<VAR>Preorder α<VAR>IsOrderBornology α<VAR>hs : BddAbove s<VAR>ht : BddBelow t<GOAL>Bornology.IsBounded (s ∩ t)
<VAR>α : Type u_1<VAR>Bornology α<VAR>ConditionallyCompleteLattice α<VAR>IsOrderBornology α<VAR>s : Set α<VAR>hs : Bornology.IsBounded s<GOAL>s ⊆ Set.Icc (sInf s) (sSup s)
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>self : α →Co β<GOAL>Continuous self.toFun
<VAR>F : Type u_6<VAR>α : outParam (Type u_7)<VAR>β : outParam (Type u_8)<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>FunLike F α β<VAR>self : ContinuousOrderHomClass F α β<VAR>f : F<GOAL>Monotone ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : α →Co β<GOAL>⇑f.toOrderHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : α →Co β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f g : α →Co β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : α →Co β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : α →Co β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<GOAL>⇑(ContinuousOrderHom.id α) = id
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>a : α<GOAL>(ContinuousOrderHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>f : β →Co γ<VAR>g : α →Co β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>f : β →Co γ<VAR>g : α →Co β<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>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>TopologicalSpace δ<VAR>Preorder δ<VAR>f : γ →Co δ<VAR>g : β →Co γ<VAR>h : α →Co β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : α →Co β<GOAL>f.comp (ContinuousOrderHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>f : α →Co β<GOAL>(ContinuousOrderHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g₁ g₂ : β →Co γ<VAR>f : α →Co β<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>TopologicalSpace α<VAR>Preorder α<VAR>TopologicalSpace β<VAR>Preorder β<VAR>TopologicalSpace γ<VAR>Preorder γ<VAR>g : β →Co γ<VAR>f₁ f₂ : α →Co β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_1<GOAL>Topology.WithUpperSet.toUpperSet.symm = Topology.WithUpperSet.ofUpperSet
<VAR>α : Type u_1<GOAL>Topology.WithUpperSet.ofUpperSet.symm = Topology.WithUpperSet.toUpperSet
<VAR>α : Type u_1<VAR>a : Topology.WithUpperSet α<GOAL>Topology.WithUpperSet.toUpperSet (Topology.WithUpperSet.ofUpperSet a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Topology.WithUpperSet.ofUpperSet (Topology.WithUpperSet.toUpperSet a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Topology.WithUpperSet.toUpperSet a = Topology.WithUpperSet.toUpperSet b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Topology.WithUpperSet α<GOAL>Topology.WithUpperSet.ofUpperSet a = Topology.WithUpperSet.ofUpperSet b ↔ a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Topology.WithUpperSet α<GOAL>Topology.WithUpperSet.ofUpperSet a ≤ Topology.WithUpperSet.ofUpperSet b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Topology.WithUpperSet.toUpperSet a ≤ Topology.WithUpperSet.toUpperSet b ↔ a ≤ b
<VAR>α : Type u_1<GOAL>Topology.WithLowerSet.toLowerSet.symm = Topology.WithLowerSet.ofLowerSet
<VAR>α : Type u_1<GOAL>Topology.WithLowerSet.ofLowerSet.symm = Topology.WithLowerSet.toLowerSet
<VAR>α : Type u_1<VAR>a : Topology.WithLowerSet α<GOAL>Topology.WithLowerSet.toLowerSet (Topology.WithLowerSet.ofLowerSet a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Topology.WithLowerSet.ofLowerSet (Topology.WithLowerSet.toLowerSet a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Topology.WithLowerSet.toLowerSet a = Topology.WithLowerSet.toLowerSet b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Topology.WithLowerSet α<GOAL>Topology.WithLowerSet.ofLowerSet a = Topology.WithLowerSet.ofLowerSet b ↔ a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Topology.WithLowerSet α<GOAL>Topology.WithLowerSet.ofLowerSet a ≤ Topology.WithLowerSet.ofLowerSet b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Topology.WithLowerSet.toLowerSet a ≤ Topology.WithLowerSet.toLowerSet b ↔ a ≤ b
<VAR>α : Type u_4<VAR>t : TopologicalSpace α<VAR>Preorder α<VAR>self : Topology.IsUpperSet α<GOAL>t = Topology.upperSet α
<VAR>α : Type u_4<VAR>t : TopologicalSpace α<VAR>Preorder α<VAR>self : Topology.IsLowerSet α<GOAL>t = Topology.lowerSet α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpperSet α<GOAL>inst✝ = Topology.upperSet α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpperSet α<VAR>s : Set α<GOAL>IsOpen s ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpperSet α<VAR>s : Set α<GOAL>IsClosed s ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpperSet α<VAR>s : Set α<GOAL>closure s = ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpperSet α<VAR>a : α<GOAL>closure {a} = Set.Iic a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Topology.IsUpperSet α<VAR>Topology.IsUpperSet β<VAR>f : α → β<GOAL>Monotone f ↔ Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Topology.IsUpperSet α<VAR>Topology.IsUpper β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Continuous f
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : TopologicalSpace α<VAR>Topology.IsUpperSet α<VAR>Topology.IsUpper α<GOAL>t₁ ≤ t₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLowerSet α<GOAL>inst✝ = Topology.lowerSet α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLowerSet α<VAR>s : Set α<GOAL>IsOpen s ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLowerSet α<VAR>s : Set α<GOAL>IsClosed s ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLowerSet α<VAR>s : Set α<GOAL>closure s = ↑(upperClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLowerSet α<VAR>a : α<GOAL>closure {a} = Set.Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Topology.IsLowerSet α<VAR>Topology.IsLowerSet β<VAR>f : α → β<GOAL>Monotone f ↔ Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Topology.IsLowerSet α<VAR>Topology.IsLower β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Continuous f
<VAR>α : Type u_1<VAR>Preorder α<VAR>t₁ t₂ : TopologicalSpace α<VAR>Topology.IsLowerSet α<VAR>Topology.IsLower α<GOAL>t₁ ≤ t₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<GOAL>Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<GOAL>Topology.IsLowerSet αᵒᵈ ↔ Topology.IsUpperSet α
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.WithUpperSet.map OrderHom.id = ContinuousMap.id (Topology.WithUpperSet α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β →o γ<VAR>f : α →o β<GOAL>Topology.WithUpperSet.map (g.comp f) = (Topology.WithUpperSet.map g).comp (Topology.WithUpperSet.map f)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Topology.WithUpperSet.toUpperSet a ⤳ Topology.WithUpperSet.toUpperSet b ↔ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Topology.WithUpperSet α<GOAL>Topology.WithUpperSet.ofUpperSet a ≤ Topology.WithUpperSet.ofUpperSet b ↔ b ⤳ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set (Topology.WithUpperSet α)<GOAL>IsUpperSet (⇑Topology.WithUpperSet.toUpperSet ⁻¹' s) ↔ IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>IsOpen (⇑Topology.WithUpperSet.ofUpperSet ⁻¹' s) ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.WithLowerSet.map OrderHom.id = ContinuousMap.id (Topology.WithLowerSet α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>g : β →o γ<VAR>f : α →o β<GOAL>Topology.WithLowerSet.map (g.comp f) = (Topology.WithLowerSet.map g).comp (Topology.WithLowerSet.map f)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Topology.WithLowerSet.toLowerSet a ⤳ Topology.WithLowerSet.toLowerSet b ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : Topology.WithLowerSet α<GOAL>Topology.WithLowerSet.ofLowerSet a ≤ Topology.WithLowerSet.ofLowerSet b ↔ a ⤳ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set (Topology.WithLowerSet α)<GOAL>IsLowerSet (⇑Topology.WithLowerSet.toLowerSet ⁻¹' s) ↔ IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>IsOpen (⇑Topology.WithLowerSet.ofLowerSet ⁻¹' s) ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>DirSupInacc sᶜ ↔ DirSupClosed s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>DirSupClosed sᶜ ↔ DirSupInacc s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>hs : DirSupClosed s<VAR>ht : DirSupClosed t<GOAL>DirSupClosed (s ∩ t)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>hs : DirSupInacc s<VAR>ht : DirSupInacc t<GOAL>DirSupInacc (s ∪ t)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>DirSupClosed s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>DirSupInacc s
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>DirSupClosed (Set.Iic a)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → sSup d ∈ s → (d ∩ s).Nonempty
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<GOAL>DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → d ⊆ s → sSup d ∈ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : Topology.IsScottHausdorff α<GOAL>inst✝ = Topology.scottHausdorff α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScottHausdorff α<GOAL>inst✝ = Topology.scottHausdorff α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScottHausdorff α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScottHausdorff α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScottHausdorff α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsClosed s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScottHausdorff α<VAR>s : Set α<VAR>h : IsOpen s<GOAL>DirSupInacc s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScottHausdorff α<VAR>s : Set α<VAR>h : IsClosed s<GOAL>DirSupClosed s
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.upperSet α ≤ Topology.scott α
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.scottHausdorff α ≤ Topology.scott α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : Topology.IsScott α<GOAL>inst✝ = Topology.scott α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<GOAL>inst✝ = Topology.scott α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>IsOpen s ↔ IsUpperSet s ∧ IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>IsOpen s ↔ IsUpperSet s ∧ DirSupInacc s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>IsOpen s → IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>IsClosed s → IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>IsClosed s → DirSupClosed s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>s : Set α<GOAL>↑(lowerClosure s) ⊆ closure s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>a : α<GOAL>IsClosed (Set.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>a : α<GOAL>closure {a} = Set.Iic a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>Preorder β<VAR>TopologicalSpace β<VAR>Topology.IsScott β<VAR>f : α → β<VAR>hf : Continuous f<GOAL>Monotone f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>Preorder β<VAR>TopologicalSpace β<VAR>Topology.IsScott β<VAR>f : α → β<GOAL>ScottContinuous f ↔ Continuous f
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<VAR>U : Set α<GOAL>IsOpen U ↔ (∃ a, U = (Set.Iic a)ᶜ) ∨ U = Set.univ
<VAR>α : Type u_1<GOAL>Topology.WithScott.toScott.symm = Topology.WithScott.ofScott
<VAR>α : Type u_1<GOAL>Topology.WithScott.ofScott.symm = Topology.WithScott.toScott
<VAR>α : Type u_1<VAR>a : Topology.WithScott α<GOAL>Topology.WithScott.toScott (Topology.WithScott.ofScott a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Topology.WithScott.ofScott (Topology.WithScott.toScott a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Topology.WithScott.toScott a = Topology.WithScott.toScott b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Topology.WithScott α<GOAL>Topology.WithScott.ofScott a = Topology.WithScott.ofScott b ↔ a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>u : Set α<GOAL>IsOpen (⇑Topology.WithScott.ofScott ⁻¹' u) ↔ IsUpperSet u ∧ TopologicalSpace.IsOpen u
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.scottHausdorff α ≤ Topology.lower α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsScott α<GOAL>Topology.scottHausdorff α ≤ inst✝
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<GOAL>Topology.scottHausdorff α ≤ inst✝
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Function.support f ⊆ tsupport f
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Function.mulSupport f ⊆ mulTSupport f
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>IsClosed (mulTSupport f)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>IsClosed (tsupport f)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>mulTSupport f = ∅ ↔ f = 1
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>tsupport f = ∅ ↔ f = 0
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>TopologicalSpace X<VAR>f : X → α<VAR>x : X<VAR>hx : x ∉ mulTSupport f<GOAL>f x = 1
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>TopologicalSpace X<VAR>f : X → α<VAR>x : X<VAR>hx : x ∉ tsupport f<GOAL>f x = 0
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Set.range f ⊆ insert 1 (f '' mulTSupport f)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Set.range f ⊆ insert 0 (f '' tsupport f)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>One α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Set.range f = f '' mulTSupport f ∨ Set.range f = insert 1 (f '' mulTSupport f)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>TopologicalSpace X<VAR>f : X → α<GOAL>Set.range f = f '' tsupport f ∨ Set.range f = insert 0 (f '' tsupport f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_10<VAR>MulZeroClass α<VAR>f g : X → α<GOAL>(tsupport fun x => f x * g x) ⊆ tsupport f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>α : Type u_10<VAR>MulZeroClass α<VAR>f g : X → α<GOAL>(tsupport fun x => f x * g x) ⊆ tsupport g
<VAR>X : Type u_1<VAR>M : Type u_10<VAR>α : Type u_11<VAR>TopologicalSpace X<VAR>Zero M<VAR>Zero α<VAR>SMulWithZero M α<VAR>f : X → M<VAR>g : X → α<GOAL>(tsupport fun x => f x • g x) ⊆ tsupport f