ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => min (f b) (g b)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => max (f b) (g b)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<GOAL>Continuous fun p => min p.1 p.2
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<GOAL>Continuous fun p => max p.1 p.2
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>b : Filter β<VAR>a₁ a₂ : α<VAR>hf : Filter.Tendsto f b (𝓝 a₁)<VAR>hg : Filter.Tendsto g b (𝓝 a₂)<GOAL>Filter.Tendsto (fun b => max (f b) (g b)) b (𝓝 (max a₁ a₂))
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>b : Filter β<VAR>a₁ a₂ : α<VAR>hf : Filter.Tendsto f b (𝓝 a₁)<VAR>hg : Filter.Tendsto g b (𝓝 a₂)<GOAL>Filter.Tendsto (fun b => min (f b) (g b)) b (𝓝 (min a₁ a₂))
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun i => max a (f i)) l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun i => max (f i) a) l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝[>] a)<GOAL>Filter.Tendsto (fun i => max a (f i)) l (𝓝[>] a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝[>] a)<GOAL>Filter.Tendsto (fun i => max (f i) a) l (𝓝[>] a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun i => min a (f i)) l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Filter.Tendsto (fun i => min (f i) a) l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝[<] a)<GOAL>Filter.Tendsto (fun i => min a (f i)) l (𝓝[<] a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝[<] a)<GOAL>Filter.Tendsto (fun i => min (f i) a) l (𝓝[<] a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<VAR>x y : α<VAR>h : x < y<GOAL>∃ z ∈ s, z ∈ Set.Ioo x y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>Set.Ioi x = ⋃ y ∈ s ∩ Set.Ioi x, Set.Ioi y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>DenselyOrdered α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>Set.Iio x = ⋃ y ∈ s ∩ Set.Iio x, Set.Iio y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>A : Set α<VAR>Cf : ContinuousAt f (sSup A)<VAR>Mf : Monotone f<VAR>A_nonemp : A.Nonempty<VAR>A_bdd : BddAbove A := by bddDefault<GOAL>f (sSup A) = sSup (f '' A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Mf : Monotone f<VAR>bdd : BddAbove (Set.range g) := by bddDefault<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>A : Set α<VAR>Cf : ContinuousAt f (sInf A)<VAR>Mf : Monotone f<VAR>A_nonemp : A.Nonempty<VAR>A_bdd : BddBelow A := by bddDefault<GOAL>f (sInf A) = sInf (f '' A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Mf : Monotone f<VAR>bdd : BddBelow (Set.range g) := by bddDefault<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>A : Set α<VAR>Cf : ContinuousAt f (sInf A)<VAR>Af : Antitone f<VAR>A_nonemp : A.Nonempty<VAR>A_bdd : BddBelow A := by bddDefault<GOAL>f (sInf A) = sSup (f '' A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Af : Antitone f<VAR>bdd : BddBelow (Set.range g) := by bddDefault<GOAL>f (⨅ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>A : Set α<VAR>Cf : ContinuousAt f (sSup A)<VAR>Af : Antitone f<VAR>A_nonemp : A.Nonempty<VAR>A_bdd : BddAbove A := by bddDefault<GOAL>f (sSup A) = sInf (f '' A)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Af : Antitone f<VAR>bdd : BddAbove (Set.range g) := by bddDefault<GOAL>f (⨆ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>sSup s ∈ closure s
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>sInf s ∈ closure s
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>hc : IsClosed s<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>hc : IsClosed s<GOAL>sInf s ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Mf : Monotone f<VAR>fbot : f ⊥ = ⊥<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sInf s)<VAR>Mf : Monotone f<VAR>ftop : f ⊤ = ⊤<GOAL>f (sInf s) = sInf (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Mf : Monotone f<VAR>ftop : f ⊤ = ⊤<GOAL>f (iInf g) = iInf (f ∘ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Af : Antitone f<VAR>fbot : f ⊥ = ⊤<GOAL>f (sSup s) = sInf (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Af : Antitone f<VAR>fbot : f ⊥ = ⊤<GOAL>f (⨆ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sInf s)<VAR>Af : Antitone f<VAR>ftop : f ⊤ = ⊥<GOAL>f (sInf s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>CompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>ι : Sort u_4<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iInf g)<VAR>Af : Antitone f<VAR>ftop : f ⊤ = ⊥<GOAL>f (iInf g) = iSup (f ∘ g)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>B : BddAbove s<GOAL>sSup s ∈ closure s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>B : BddBelow s<GOAL>sInf s ∈ closure s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hc : IsClosed s<VAR>hs : s.Nonempty<VAR>B : BddAbove s<GOAL>sSup s ∈ s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hc : IsClosed s<VAR>hs : s.Nonempty<VAR>B : BddBelow s<GOAL>sInf s ∈ s
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hc : IsClosed s<VAR>hs : s.Nonempty<VAR>B : BddBelow s<GOAL>IsLeast s (sInf s)
<VAR>α : Type u_1<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>hc : IsClosed s<VAR>hs : s.Nonempty<VAR>B : BddAbove s<GOAL>IsGreatest s (sSup s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Mf : Monotone f<VAR>ne : s.Nonempty<VAR>H : BddAbove s<GOAL>f (sSup s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>Nonempty γ<VAR>f : α → β<VAR>g : γ → α<VAR>Cf : ContinuousAt f (⨆ i, g i)<VAR>Mf : Monotone f<VAR>H : BddAbove (Set.range g)<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sInf s)<VAR>Mf : Monotone f<VAR>ne : s.Nonempty<VAR>H : BddBelow s<GOAL>f (sInf s) = sInf (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>Nonempty γ<VAR>f : α → β<VAR>g : γ → α<VAR>Cf : ContinuousAt f (⨅ i, g i)<VAR>Mf : Monotone f<VAR>H : BddBelow (Set.range g)<GOAL>f (⨅ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sSup s)<VAR>Af : Antitone f<VAR>ne : s.Nonempty<VAR>H : BddAbove s<GOAL>f (sSup s) = sInf (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>Nonempty γ<VAR>f : α → β<VAR>g : γ → α<VAR>Cf : ContinuousAt f (⨆ i, g i)<VAR>Af : Antitone f<VAR>H : BddAbove (Set.range g)<GOAL>f (⨆ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>f : α → β<VAR>s : Set α<VAR>Cf : ContinuousAt f (sInf s)<VAR>Af : Antitone f<VAR>ne : s.Nonempty<VAR>H : BddBelow s<GOAL>f (sInf s) = sSup (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderClosedTopology β<VAR>Nonempty γ<VAR>f : α → β<VAR>g : γ → α<VAR>Cf : ContinuousAt f (⨅ i, g i)<VAR>Af : Antitone f<VAR>H : BddBelow (Set.range g)<GOAL>f (⨅ i, g i) = ⨆ i, f (g i)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Set.Iio x)))
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>Mf : Monotone f<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Set.Ioi x)))
<VAR>α : Type u_3<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : SupConvergenceClass α<VAR>a : α<VAR>s : Set α<GOAL>IsLUB s a → Filter.Tendsto CoeTC.coe Filter.atTop (𝓝 a)
<VAR>α : Type u_3<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : InfConvergenceClass α<VAR>a : α<VAR>s : Set α<GOAL>IsGLB s a → Filter.Tendsto CoeTC.coe Filter.atBot (𝓝 a)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>Preorder α<VAR>SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>ha : IsLUB (Set.range f) a<GOAL>Filter.Tendsto f Filter.atTop (𝓝 a)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>Preorder α<VAR>SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_anti : Antitone f<VAR>ha : IsLUB (Set.range f) a<GOAL>Filter.Tendsto f Filter.atBot (𝓝 a)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>Preorder α<VAR>InfConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_mono : Monotone f<VAR>ha : IsGLB (Set.range f) a<GOAL>Filter.Tendsto f Filter.atBot (𝓝 a)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>Preorder α<VAR>InfConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_anti : Antitone f<VAR>ha : IsGLB (Set.range f) a<GOAL>Filter.Tendsto f Filter.atTop (𝓝 a)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLattice α<VAR>SupConvergenceClass α<VAR>f : ι → α<VAR>h_mono : Monotone f<VAR>hbdd : BddAbove (Set.range f)<GOAL>Filter.Tendsto f Filter.atTop (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLattice α<VAR>SupConvergenceClass α<VAR>f : ι → α<VAR>h_anti : Antitone f<VAR>hbdd : BddAbove (Set.range f)<GOAL>Filter.Tendsto f Filter.atBot (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLattice α<VAR>InfConvergenceClass α<VAR>f : ι → α<VAR>h_mono : Monotone f<VAR>hbdd : BddBelow (Set.range f)<GOAL>Filter.Tendsto f Filter.atBot (𝓝 (⨅ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLattice α<VAR>InfConvergenceClass α<VAR>f : ι → α<VAR>h_anti : Antitone f<VAR>hbdd : BddBelow (Set.range f)<GOAL>Filter.Tendsto f Filter.atTop (𝓝 (⨅ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>CompleteLattice α<VAR>SupConvergenceClass α<VAR>f : ι → α<VAR>h_mono : Monotone f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>CompleteLattice α<VAR>SupConvergenceClass α<VAR>f : ι → α<VAR>h_anti : Antitone f<GOAL>Filter.Tendsto f Filter.atBot (𝓝 (⨆ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>CompleteLattice α<VAR>InfConvergenceClass α<VAR>f : ι → α<VAR>h_mono : Monotone f<GOAL>Filter.Tendsto f Filter.atBot (𝓝 (⨅ i, f i))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>CompleteLattice α<VAR>InfConvergenceClass α<VAR>f : ι → α<VAR>h_anti : Antitone f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 (⨅ i, f i))
<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>f : ι → α<VAR>h_mono : Monotone f<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop ∨ ∃ l, Filter.Tendsto f Filter.atTop (𝓝 l)
<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>Preorder ι<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>f : ι → α<VAR>h_mono : Antitone f<GOAL>Filter.Tendsto f Filter.atTop Filter.atBot ∨ ∃ l, Filter.Tendsto f Filter.atTop (𝓝 l)
<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>α : Type u_5<VAR>SemilatticeSup ι₁<VAR>Preorder ι₂<VAR>Nonempty ι₁<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>NoMaxOrder α<VAR>f : ι₂ → α<VAR>φ : ι₁ → ι₂<VAR>l : α<VAR>hf : Monotone f<VAR>hg : Filter.Tendsto φ Filter.atTop Filter.atTop<GOAL>Filter.Tendsto f Filter.atTop (𝓝 l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (𝓝 l)
<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>α : Type u_5<VAR>SemilatticeSup ι₁<VAR>Preorder ι₂<VAR>Nonempty ι₁<VAR>TopologicalSpace α<VAR>ConditionallyCompleteLinearOrder α<VAR>OrderTopology α<VAR>NoMinOrder α<VAR>f : ι₂ → α<VAR>φ : ι₁ → ι₂<VAR>l : α<VAR>hf : Antitone f<VAR>hg : Filter.Tendsto φ Filter.atTop Filter.atTop<GOAL>Filter.Tendsto f Filter.atTop (𝓝 l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (𝓝 l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>SemilatticeSup β<VAR>f : β → α<VAR>a : α<VAR>hf : Monotone f<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>b : β<GOAL>f b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>SemilatticeInf β<VAR>f : β → α<VAR>a : α<VAR>hf : Monotone f<VAR>ha : Filter.Tendsto f Filter.atBot (𝓝 a)<VAR>b : β<GOAL>a ≤ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>SemilatticeSup β<VAR>f : β → α<VAR>a : α<VAR>hf : Antitone f<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<VAR>b : β<GOAL>a ≤ f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>SemilatticeInf β<VAR>f : β → α<VAR>a : α<VAR>hf : Antitone f<VAR>ha : Filter.Tendsto f Filter.atBot (𝓝 a)<VAR>b : β<GOAL>f b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → α<VAR>a : α<VAR>hf : Monotone f<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>IsLUB (Set.range f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>Nonempty β<VAR>SemilatticeInf β<VAR>f : β → α<VAR>a : α<VAR>hf : Monotone f<VAR>ha : Filter.Tendsto f Filter.atBot (𝓝 a)<GOAL>IsGLB (Set.range f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>Nonempty β<VAR>SemilatticeInf β<VAR>f : β → α<VAR>a : α<VAR>hf : Antitone f<VAR>ha : Filter.Tendsto f Filter.atBot (𝓝 a)<GOAL>IsLUB (Set.range f) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>Preorder α<VAR>OrderClosedTopology α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → α<VAR>a : α<VAR>hf : Antitone f<VAR>ha : Filter.Tendsto f Filter.atTop (𝓝 a)<GOAL>IsGLB (Set.range f) a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>TopologicalSpace α<VAR>CompleteLinearOrder α<VAR>OrderTopology α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → α<VAR>a : α<VAR>hf : Monotone f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 a) → iSup f = a
<VAR>β : Type u_2<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>CompleteLinearOrder α<VAR>OrderTopology α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>f : β → α<VAR>a : α<VAR>hf : Antitone f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 a) → iInf f = a
<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>α : Type u_5<VAR>Preorder ι₂<VAR>CompleteLattice α<VAR>l : Filter ι₁<VAR>l.NeBot<VAR>f : ι₂ → α<VAR>φ : ι₁ → ι₂<VAR>hf : Monotone f<VAR>hφ : Filter.Tendsto φ l Filter.atTop<GOAL>⨆ i, f i = ⨆ i, f (φ i)
<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>α : Type u_5<VAR>Preorder ι₂<VAR>CompleteLattice α<VAR>l : Filter ι₁<VAR>l.NeBot<VAR>f : ι₂ → α<VAR>φ : ι₁ → ι₂<VAR>hf : Antitone f<VAR>hφ : Filter.Tendsto φ l Filter.atBot<GOAL>⨆ i, f i = ⨆ i, f (φ i)
<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>α : Type u_5<VAR>Preorder ι₂<VAR>CompleteLattice α<VAR>l : Filter ι₁<VAR>l.NeBot<VAR>f : ι₂ → α<VAR>φ : ι₁ → ι₂<VAR>hf : Monotone f<VAR>hφ : Filter.Tendsto φ l Filter.atBot<GOAL>⨅ i, f i = ⨅ i, f (φ i)
<VAR>ι₁ : Type u_3<VAR>ι₂ : Type u_4<VAR>α : Type u_5<VAR>Preorder ι₂<VAR>CompleteLattice α<VAR>l : Filter ι₁<VAR>l.NeBot<VAR>f : ι₂ → α<VAR>φ : ι₁ → ι₂<VAR>hf : Antitone f<VAR>hφ : Filter.Tendsto φ l Filter.atTop<GOAL>⨅ i, f i = ⨅ i, f (φ i)
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>LE α<VAR>self : ClopenUpperSet α<GOAL>IsUpperSet self.carrier
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s : ClopenUpperSet α<GOAL>IsUpperSet ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s : ClopenUpperSet α<GOAL>IsClopen ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s : ClopenUpperSet α<GOAL>↑s.toUpperSet = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s t : ClopenUpperSet α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s : TopologicalSpace.Clopens α<VAR>h : IsUpperSet s.carrier<GOAL>↑{ toClopens := s, upper' := h } = ↑s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s t : ClopenUpperSet α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<VAR>s t : ClopenUpperSet α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LE α<GOAL>↑⊥ = ∅
<VAR>α : Type u_1<GOAL>Topology.WithLower.toLower.symm = Topology.WithLower.ofLower
<VAR>α : Type u_1<GOAL>Topology.WithLower.ofLower.symm = Topology.WithLower.toLower
<VAR>α : Type u_1<VAR>a : Topology.WithLower α<GOAL>Topology.WithLower.toLower (Topology.WithLower.ofLower a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Topology.WithLower.ofLower (Topology.WithLower.toLower a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Topology.WithLower.toLower a = Topology.WithLower.toLower b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Topology.WithLower α<GOAL>Topology.WithLower.ofLower a = Topology.WithLower.ofLower b ↔ a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>IsOpen (⇑Topology.WithLower.ofLower ⁻¹' s) ↔ TopologicalSpace.IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>T : Set (Topology.WithLower α)<GOAL>IsOpen T ↔ TopologicalSpace.IsOpen (⇑Topology.WithLower.toLower ⁻¹' T)
<VAR>α : Type u_1<GOAL>Topology.WithUpper.toUpper.symm = Topology.WithUpper.ofUpper
<VAR>α : Type u_1<GOAL>Topology.WithUpper.ofUpper.symm = Topology.WithUpper.toUpper