ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>hg : IsLocalMax g a<GOAL>IsLocalMax (fun x => min (f x) (g x)) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMinOn (fun x => min (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMaxOn (fun x => min (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>hg : IsLocalMin g a<GOAL>IsLocalMin (fun x => max (f x) (g x)) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>hg : IsLocalMax g a<GOAL>IsLocalMax (fun x => max (f x) (g x)) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMinOn (fun x => max (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMaxOn (fun x => max (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>hle : g ≤ᶠ[𝓝[s] a] f<VAR>hfga : f a = g a<VAR>h : IsLocalMaxOn f s a<GOAL>IsLocalMaxOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>h : IsLocalMaxOn f s a<VAR>heq : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>IsLocalMaxOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>heq : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>IsLocalMaxOn f s a ↔ IsLocalMaxOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>hle : f ≤ᶠ[𝓝[s] a] g<VAR>hfga : f a = g a<VAR>h : IsLocalMinOn f s a<GOAL>IsLocalMinOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>h : IsLocalMinOn f s a<VAR>heq : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>IsLocalMinOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>heq : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>IsLocalMinOn f s a ↔ IsLocalMinOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>h : IsLocalExtrOn f s a<VAR>heq : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>IsLocalExtrOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>heq : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>IsLocalExtrOn f s a ↔ IsLocalExtrOn g s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>hle : g ≤ᶠ[𝓝 a] f<VAR>hfga : f a = g a<VAR>h : IsLocalMax f a<GOAL>IsLocalMax g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>h : IsLocalMax f a<VAR>heq : f =ᶠ[𝓝 a] g<GOAL>IsLocalMax g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>heq : f =ᶠ[𝓝 a] g<GOAL>IsLocalMax f a ↔ IsLocalMax g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>hle : f ≤ᶠ[𝓝 a] g<VAR>hfga : f a = g a<VAR>h : IsLocalMin f a<GOAL>IsLocalMin g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>h : IsLocalMin f a<VAR>heq : f =ᶠ[𝓝 a] g<GOAL>IsLocalMin g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>heq : f =ᶠ[𝓝 a] g<GOAL>IsLocalMin f a ↔ IsLocalMin g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>h : IsLocalExtr f a<VAR>heq : f =ᶠ[𝓝 a] g<GOAL>IsLocalExtr g a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f g : α → β<VAR>a : α<VAR>heq : f =ᶠ[𝓝 a] g<GOAL>IsLocalExtr f a ↔ IsLocalExtr g a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsLUB s a<VAR>hs : s.Nonempty<GOAL>∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsLUB s a<VAR>hs : s.Nonempty<GOAL>∃ᶠ (x : α) in 𝓝 a, x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsGLB s a<VAR>hs : s.Nonempty<GOAL>∃ᶠ (x : α) in 𝓝[≥] a, x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsGLB s a<VAR>hs : s.Nonempty<GOAL>∃ᶠ (x : α) in 𝓝 a, x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsLUB s a<VAR>hs : s.Nonempty<GOAL>a ∈ closure s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsGLB s a<VAR>hs : s.Nonempty<GOAL>a ∈ closure s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsLUB s a<VAR>hs : s.Nonempty<GOAL>(𝓝[s] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<GOAL>IsGLB s a → s.Nonempty → (𝓝[s] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>s : Set α<VAR>a : α<VAR>f : Filter α<VAR>hsa : a ∈ upperBounds s<VAR>hsf : s ∈ f<VAR>(f ⊓ 𝓝 a).NeBot<GOAL>IsLUB s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>s : Set α<VAR>a : α<VAR>hsa : a ∈ upperBounds s<VAR>hsf : a ∈ closure s<GOAL>IsLUB s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>s : Set α<VAR>a : α<VAR>f : Filter α<GOAL>a ∈ lowerBounds s → s ∈ f → (f ⊓ 𝓝 a).NeBot → IsGLB s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>s : Set α<VAR>a : α<VAR>hsa : a ∈ lowerBounds s<VAR>hsf : a ∈ closure s<GOAL>IsGLB s a
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>ha : IsLUB s a<VAR>hb : Filter.Tendsto f (𝓝[s] a) (𝓝 b)<GOAL>b ∈ upperBounds (f '' s)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>ha : IsLUB s a<VAR>hs : s.Nonempty<VAR>hb : Filter.Tendsto f (𝓝[s] a) (𝓝 b)<GOAL>IsLUB (f '' s) b
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<VAR>ha : IsGLB s a<VAR>hb : Filter.Tendsto f (𝓝[s] a) (𝓝 b)<GOAL>b ∈ lowerBounds (f '' s)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : MonotoneOn f s<GOAL>IsGLB s a → s.Nonempty → Filter.Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : AntitoneOn f s<VAR>ha : IsLUB s a<VAR>hb : Filter.Tendsto f (𝓝[s] a) (𝓝 b)<GOAL>b ∈ lowerBounds (f '' s)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<GOAL>AntitoneOn f s → IsLUB s a → s.Nonempty → Filter.Tendsto f (𝓝[s] a) (𝓝 b) → IsGLB (f '' s) b
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<VAR>hf : AntitoneOn f s<VAR>ha : IsGLB s a<VAR>hb : Filter.Tendsto f (𝓝[s] a) (𝓝 b)<GOAL>b ∈ upperBounds (f '' s)
<VAR>α : Type u_1<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>Preorder γ<VAR>TopologicalSpace γ<VAR>OrderClosedTopology γ<VAR>f : α → γ<VAR>s : Set α<VAR>a : α<VAR>b : γ<GOAL>AntitoneOn f s → IsGLB s a → s.Nonempty → Filter.Tendsto f (𝓝[s] a) (𝓝 b) → IsLUB (f '' s) b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsLUB s a<VAR>hs : s.Nonempty<VAR>sc : IsClosed s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>ha : IsGLB s a<VAR>hs : s.Nonempty<VAR>sc : IsClosed s<GOAL>a ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>t : Set α<VAR>x : α<VAR>(𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>t : Set α<VAR>x : α<VAR>(𝓝 x).IsCountablyGenerated<VAR>htx : IsLUB t x<VAR>ht : t.Nonempty<GOAL>∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Filter.Tendsto u Filter.atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_4<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>DenselyOrdered α<VAR>OrderTopology α<VAR>FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo y x) ∧ Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>FirstCountableTopology α<VAR>x : α<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>FirstCountableTopology α<VAR>x : α<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (𝓝[<] x)
<VAR>α : Type u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>FirstCountableTopology α<VAR>S : Set α<VAR>hS : S.Nonempty<VAR>hS' : BddAbove S<GOAL>∃ u, Monotone u ∧ Filter.Tendsto u Filter.atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>t : Set α<VAR>x : α<VAR>(𝓝 x).IsCountablyGenerated<VAR>htx : IsGLB t x<VAR>not_mem : x ∉ t<VAR>ht : t.Nonempty<GOAL>∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>t : Set α<VAR>x : α<VAR>(𝓝 x).IsCountablyGenerated<VAR>htx : IsGLB t x<VAR>ht : t.Nonempty<GOAL>∃ u, Antitone u ∧ (∀ (n : ℕ), x ≤ u n) ∧ Filter.Tendsto u Filter.atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>FirstCountableTopology α<VAR>x y : α<VAR>hy : x < y<GOAL>∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y) ∧ Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>FirstCountableTopology α<VAR>x : α<GOAL>∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>FirstCountableTopology α<VAR>x : α<GOAL>∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (𝓝[>] x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>FirstCountableTopology α<VAR>x y : α<VAR>h : x < y<GOAL>∃ u v, StrictAnti u ∧ StrictMono v ∧ (∀ (k : ℕ), u k ∈ Set.Ioo x y) ∧ (∀ (l : ℕ), v l ∈ Set.Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Filter.Tendsto u Filter.atTop (𝓝 x) ∧ Filter.Tendsto v Filter.atTop (𝓝 y)
<VAR>α : Type u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>FirstCountableTopology α<VAR>S : Set α<VAR>hS : S.Nonempty<VAR>hS' : BddBelow S<GOAL>∃ u, Antitone u ∧ Filter.Tendsto u Filter.atTop (𝓝 (sInf S)) ∧ ∀ (n : ℕ), u n ∈ S
<VAR>X : AlexDisc<GOAL>↑((CategoryTheory.forget₂ AlexDisc TopCat).obj X) = ↑X
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<GOAL>↑(AlexDisc.of α) = α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>AlexandrovDiscrete α<GOAL>(CategoryTheory.forget₂ AlexDisc TopCat).obj (AlexDisc.of α) = TopCat.of α
<VAR>α β : AlexDisc<VAR>e : ↑α ≃ₜ ↑β<GOAL>(AlexDisc.Iso.mk e).inv = e.symm.toContinuousMap
<VAR>α β : AlexDisc<VAR>e : ↑α ≃ₜ ↑β<GOAL>(AlexDisc.Iso.mk e).hom = e.toContinuousMap
<GOAL>alexDiscEquivPreord.functor = CategoryTheory.forget₂ AlexDisc TopCat ⋙ topToPreord
<GOAL>∀ {X Y : Preord} (f : ↑X →o ↑Y), alexDiscEquivPreord.inverse.map f = Topology.WithUpperSet.map f
<GOAL>alexDiscEquivPreord.unitIso = CategoryTheory.NatIso.ofComponents (fun X => AlexDisc.Iso.mk (id (homeoWithUpperSetTopologyorderIso ↑X))) @alexDiscEquivPreord.proof_4
<GOAL>alexDiscEquivPreord.counitIso = CategoryTheory.NatIso.ofComponents (fun X => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm)) @alexDiscEquivPreord.proof_5
<VAR>X : Preord<GOAL>alexDiscEquivPreord.inverse.obj X = AlexDisc.of (Topology.WithUpperSet ↑X)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>self : Topology.IsLawson α<GOAL>inst✝ = Topology.lawson α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLawson α<GOAL>TopologicalSpace.IsTopologicalBasis (Topology.IsLawson.lawsonBasis α)
<VAR>α : Type u_1<GOAL>Topology.WithLawson.toLawson.symm = Topology.WithLawson.ofLawson
<VAR>α : Type u_1<GOAL>Topology.WithLawson.ofLawson.symm = Topology.WithLawson.toLawson
<VAR>α : Type u_1<VAR>a : Topology.WithLawson α<GOAL>Topology.WithLawson.toLawson (Topology.WithLawson.ofLawson a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Topology.WithLawson.ofLawson (Topology.WithLawson.toLawson a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Topology.WithLawson.toLawson a = Topology.WithLawson.toLawson b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Topology.WithLawson α<GOAL>Topology.WithLawson.ofLawson a = Topology.WithLawson.ofLawson b ↔ a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>S : Set α<GOAL>IsOpen (⇑Topology.WithLawson.ofLawson ⁻¹' S) ↔ TopologicalSpace.IsOpen S
<VAR>α : Type u_1<VAR>Preorder α<VAR>S : Set α<GOAL>IsClosed (⇑Topology.WithLawson.ofLawson ⁻¹' S) ↔ IsClosed S
<VAR>α : Type u_1<VAR>Preorder α<VAR>T : Set (Topology.WithLawson α)<GOAL>IsOpen T ↔ TopologicalSpace.IsOpen (⇑Topology.WithLawson.toLawson ⁻¹' T)
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.lawson α ≤ Topology.scott α
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.lawson α ≤ Topology.lower α
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Topology.scottHausdorff α ≤ Topology.lawson α
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsClosed (⇑Topology.WithScott.ofScott ⁻¹' s)<GOAL>IsClosed (⇑Topology.WithLawson.ofLawson ⁻¹' s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsClosed (⇑Topology.WithLower.ofLower ⁻¹' s)<GOAL>IsClosed (⇑Topology.WithLawson.ofLawson ⁻¹' s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsOpen (⇑Topology.WithLawson.ofLawson ⁻¹' s) ↔ IsOpen (⇑Topology.WithScott.ofScott ⁻¹' s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>L S : TopologicalSpace α<VAR>Topology.IsLawson α<VAR>Topology.IsScott α<GOAL>L ≤ S
<VAR>α : Type u_1<VAR>Preorder α<VAR>L : TopologicalSpace α<VAR>Topology.IsLawson α<GOAL>Topology.scottHausdorff α ≤ L
<VAR>α : Type u_1<VAR>Preorder α<VAR>L S : TopologicalSpace α<VAR>Topology.IsLawson α<VAR>Topology.IsScott α<VAR>s : Set α<VAR>h : IsUpperSet s<GOAL>IsOpen s ↔ IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>L S : TopologicalSpace α<VAR>Topology.IsLawson α<VAR>Topology.IsScott α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsClosed s ↔ IsClosed s
<VAR>α : Type u_1<VAR>Preorder α<VAR>L S : TopologicalSpace α<VAR>Topology.IsLawson α<VAR>Topology.IsScott α<VAR>s : Set α<VAR>h : IsLowerSet s<GOAL>IsClosed s ↔ DirSupClosed s
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>TopologicalSpace α<VAR>Topology.IsLawson α<VAR>a : α<GOAL>IsClosed {a}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Preorder Y<VAR>OrderClosedTopology Y<VAR>f : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsMaxOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Preorder Y<VAR>OrderClosedTopology Y<VAR>f : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsMinOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsMinOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Preorder Y<VAR>OrderClosedTopology Y<VAR>f : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsExtrOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsExtrOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Preorder Y<VAR>OrderClosedTopology Y<VAR>f : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsLocalMaxOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Preorder Y<VAR>OrderClosedTopology Y<VAR>f : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMinOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsLocalMinOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Preorder Y<VAR>OrderClosedTopology Y<VAR>f : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalExtrOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsLocalExtrOn f (closure s) a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>𝓝ˢ (Set.Ioi a) = 𝓟 (Set.Ioi a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>𝓝ˢ (Set.Iio a) = 𝓟 (Set.Iio a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>𝓝ˢ (Set.Ioo a b) = 𝓟 (Set.Ioo a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>𝓝ˢ (Set.Ici a) = 𝓝 a ⊔ 𝓟 (Set.Ioi a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>𝓝ˢ (Set.Iic a) = 𝓝 a ⊔ 𝓟 (Set.Iio a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝ˢ (Set.Ico a b) = 𝓝 a ⊔ 𝓟 (Set.Ioo a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝ˢ (Set.Ioc a b) = 𝓝 b ⊔ 𝓟 (Set.Ioo a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<VAR>h : a ≤ b<GOAL>𝓝ˢ (Set.Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Set.Ioo a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>Set.Ioi a ∈ 𝓝ˢ (Set.Ici b) ↔ a < b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ici a ∈ 𝓝ˢ (Set.Ici b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>Set.Iio b ∈ 𝓝ˢ (Set.Iic a) ↔ a < b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Iic b ∈ 𝓝ˢ (Set.Iic a)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : a < b<GOAL>Set.Ioi a ∈ 𝓝ˢ (Set.Icc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : a < b<GOAL>Set.Ici a ∈ 𝓝ˢ (Set.Icc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : b < c<GOAL>Set.Iio c ∈ 𝓝ˢ (Set.Icc a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : b < c<GOAL>Set.Iic c ∈ 𝓝ˢ (Set.Icc a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c < d<GOAL>Set.Ioo a d ∈ 𝓝ˢ (Set.Icc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c < d<GOAL>Set.Ico a d ∈ 𝓝ˢ (Set.Icc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c < d<GOAL>Set.Ioc a d ∈ 𝓝ˢ (Set.Icc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c < d<GOAL>Set.Icc a d ∈ 𝓝ˢ (Set.Icc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : a < b<GOAL>Set.Ici a ∈ 𝓝ˢ (Set.Ico b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : a < b<GOAL>Set.Ioi a ∈ 𝓝ˢ (Set.Ico b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : b ≤ c<GOAL>Set.Iio c ∈ 𝓝ˢ (Set.Ico a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : b ≤ c<GOAL>Set.Iic c ∈ 𝓝ˢ (Set.Ico a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c ≤ d<GOAL>Set.Ioo a d ∈ 𝓝ˢ (Set.Ico b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c ≤ d<GOAL>Set.Icc a d ∈ 𝓝ˢ (Set.Ico b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c ≤ d<GOAL>Set.Ioc a d ∈ 𝓝ˢ (Set.Ico b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a < b<VAR>h' : c ≤ d<GOAL>Set.Ico a d ∈ 𝓝ˢ (Set.Ico b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Set.Ioi a ∈ 𝓝ˢ (Set.Ioc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : b < c<GOAL>Set.Iio c ∈ 𝓝ˢ (Set.Ioc a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Set.Ici a ∈ 𝓝ˢ (Set.Ioc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c : α<VAR>h : b < c<GOAL>Set.Iic c ∈ 𝓝ˢ (Set.Ioc a b)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>h' : c < d<GOAL>Set.Ioo a d ∈ 𝓝ˢ (Set.Ioc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>h' : c < d<GOAL>Set.Icc a d ∈ 𝓝ˢ (Set.Ioc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>h' : c < d<GOAL>Set.Ioc a d ∈ 𝓝ˢ (Set.Ioc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>h' : c < d<GOAL>Set.Ico a d ∈ 𝓝ˢ (Set.Ioc b c)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a : α<VAR>h : Nonempty ↑(Set.Ioi a)<GOAL>(𝓝ˢ (Set.Iic a)).HasBasis (fun x => a < x) Set.Iio
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a : α<VAR>(𝓝[>] a).NeBot<GOAL>(𝓝ˢ (Set.Iic a)).HasBasis (fun x => a < x) Set.Iic
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a b : α<VAR>(𝓝[>] b).NeBot<GOAL>Set.Iic a ∈ 𝓝ˢ (Set.Iic b) ↔ b < a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>a : α<VAR>Nonempty ↑(Set.Iio a)<GOAL>(𝓝ˢ (Set.Ici a)).HasBasis (fun x => x < a) Set.Ioi