ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set α<VAR>t : Set β<VAR>hne : (s ×ˢ t).Nonempty<GOAL>Bornology.IsBounded (s ×ˢ t) ↔ Bornology.IsBounded s ∧ Bornology.IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Bornology α<VAR>Bornology β<VAR>s : Set α<VAR>t : Set β<GOAL>Bornology.IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsBounded s ∧ Bornology.IsBounded t
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<GOAL>Bornology.IsBounded (s ×ˢ s) ↔ Bornology.IsBounded s
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → Bornology (π i)<GOAL>Bornology.cobounded ((i : ι) → π i) = Filter.coprodᵢ fun i => Bornology.cobounded (π i)
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → Bornology (π i)<VAR>s : Set ((i : ι) → π i)<GOAL>(∀ (i : ι), Bornology.IsBounded (Function.eval i '' s)) ↔ Bornology.IsBounded s
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → Bornology (π i)<VAR>s : Set ((i : ι) → π i)<VAR>hs : Bornology.IsBounded s<VAR>i : ι<GOAL>Bornology.IsBounded (Function.eval i '' s)
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → Bornology (π i)<VAR>S : (i : ι) → Set (π i)<VAR>h : ∀ (i : ι), Bornology.IsBounded (S i)<GOAL>Bornology.IsBounded (Set.univ.pi S)
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → Bornology (π i)<VAR>S : (i : ι) → Set (π i)<VAR>hne : (Set.univ.pi S).Nonempty<GOAL>Bornology.IsBounded (Set.univ.pi S) ↔ ∀ (i : ι), Bornology.IsBounded (S i)
<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>(i : ι) → Bornology (π i)<VAR>S : (i : ι) → Set (π i)<GOAL>Bornology.IsBounded (Set.univ.pi S) ↔ (∃ i, S i = ∅) ∨ ∀ (i : ι), Bornology.IsBounded (S i)
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Bornology β<VAR>f : α → β<VAR>s : Set α<GOAL>Bornology.IsBounded s ↔ Bornology.IsBounded (f '' s)
<VAR>α : Type u_1<VAR>Bornology α<VAR>p : α → Prop<VAR>s : Set { x // p x }<GOAL>Bornology.IsBounded (Subtype.val '' s) ↔ Bornology.IsBounded s
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>Bornology β<VAR>f : α → β<GOAL>BoundedSpace α ↔ Bornology.IsBounded (Set.range f)
<VAR>α : Type u_1<VAR>Bornology α<VAR>p : α → Prop<GOAL>BoundedSpace (Subtype p) ↔ Bornology.IsBounded {x | p x}
<VAR>α : Type u_1<VAR>Bornology α<VAR>s : Set α<GOAL>BoundedSpace ↑s ↔ Bornology.IsBounded s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : ClosedIicTopology α<VAR>a : α<GOAL>IsClosed (Set.Iic a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : ClosedIciTopology α<VAR>a : α<GOAL>IsClosed (Set.Ici a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Preorder α<VAR>self : OrderClosedTopology α<GOAL>IsClosed {p | p.1 ≤ p.2}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : Dense s<GOAL>Dense (⇑OrderDual.ofDual ⁻¹' s)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>s : Set α<GOAL>BddAbove (closure s) → BddAbove s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>s : Set α<GOAL>BddBelow (closure s) → BddBelow s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>IsClosed (Set.Iic a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>IsClosed {x | x ≤ a}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>closure (Set.Iic a) = Set.Iic a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>a b : α<VAR>x : Filter β<VAR>lim : Filter.Tendsto f x (𝓝 a)<VAR>h : ∃ᶠ (c : β) in x, f c ≤ b<GOAL>a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>a b : α<VAR>x : Filter β<VAR>x.NeBot<VAR>lim : Filter.Tendsto f x (𝓝 a)<VAR>h : ∀ᶠ (c : β) in x, f c ≤ b<GOAL>a ≤ b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>a b : α<VAR>x : Filter β<VAR>x.NeBot<VAR>lim : Filter.Tendsto f x (𝓝 a)<VAR>h : ∀ (c : β), f c ≤ b<GOAL>a ≤ b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>s : Set α<GOAL>upperBounds (closure s) = upperBounds s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>s : Set α<GOAL>BddAbove (closure s) ↔ BddAbove s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>Disjoint (𝓝 a) Filter.atBot ↔ ¬IsBot a
<VAR>α : Type u<VAR>Preorder α<VAR>NoBotOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>Disjoint (𝓝 a) Filter.atBot
<VAR>α : Type u<VAR>Preorder α<VAR>NoBotOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>𝓝 a ⊓ Filter.atBot = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>NoBotOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>l : Filter β<VAR>l.NeBot<VAR>f : β → α<VAR>hf : Filter.Tendsto f l Filter.atBot<VAR>a : α<GOAL>¬Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>NoBotOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>a : α<VAR>l : Filter β<VAR>l.NeBot<VAR>f : β → α<VAR>hf : Filter.Tendsto f l (𝓝 a)<GOAL>¬Filter.Tendsto f l Filter.atBot
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>IsOpen (Set.Ioi a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a : α<GOAL>interior (Set.Ioi a) = Set.Ioi a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ioi a ∈ 𝓝 b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>hab : b < a<GOAL>∀ᶠ (x : α) in 𝓝 a, b < x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Ici a ∈ 𝓝 b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>hab : b < a<GOAL>∀ᶠ (x : α) in 𝓝 a, b ≤ x
<VAR>α : Type u<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>l : Filter γ<VAR>f : γ → α<VAR>u v : α<VAR>hv : u < v<VAR>h : Filter.Tendsto f l (𝓝 v)<GOAL>∀ᶠ (a : γ) in l, u < f a
<VAR>α : Type u<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>l : Filter γ<VAR>f : γ → α<VAR>u v : α<VAR>hv : u < v<VAR>h : Filter.Tendsto f l (𝓝 v)<GOAL>∀ᶠ (a : γ) in l, u ≤ f a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>NoMaxOrder α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>∃ y ∈ s, x < y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>NoMaxOrder α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>∃ y ∈ s, x ≤ y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>s : Set α<VAR>hs : Dense s<VAR>htop : ∀ (x : α), IsTop x → x ∈ s<VAR>x : α<GOAL>∃ y ∈ s, x ≤ y
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ioo a b ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioc a c<GOAL>Set.Ioo a c ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>𝓝[<] b = ⊥
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioc a c<GOAL>Set.Ico a c ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ico a b ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioc a c<GOAL>Set.Ioc a c ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ioc a b ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioc a c<GOAL>Set.Icc a c ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Icc a b ∈ 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Ico a b] b = 𝓝[<] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Ioo a b] b = 𝓝[<] b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Ico a b) b ↔ ContinuousWithinAt f (Set.Iio b) b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Ioo a b) b ↔ ContinuousWithinAt f (Set.Iio b) b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ioc a b ∈ 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioo a c<GOAL>Set.Ioo a c ∈ 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioo a c<GOAL>Set.Ico a c ∈ 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioc a c<GOAL>Set.Ioc a c ∈ 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioc a c<GOAL>Set.Icc a c ∈ 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Icc a b ∈ 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Icc a b] b = 𝓝[≤] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Ioc a b] b = 𝓝[≤] b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Icc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIicTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Ioc a b) b ↔ ContinuousWithinAt f (Set.Iic b) b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>IsClosed (Set.Ici a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>IsClosed {x | a ≤ x}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>closure (Set.Ici a) = Set.Ici a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>a b : α<VAR>x : Filter β<VAR>lim : Filter.Tendsto f x (𝓝 a)<VAR>h : ∃ᶠ (c : β) in x, b ≤ f c<GOAL>b ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>a b : α<VAR>x : Filter β<VAR>x.NeBot<VAR>lim : Filter.Tendsto f x (𝓝 a)<VAR>h : ∀ᶠ (c : β) in x, b ≤ f c<GOAL>b ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>a b : α<VAR>x : Filter β<VAR>x.NeBot<VAR>lim : Filter.Tendsto f x (𝓝 a)<VAR>h : ∀ (c : β), b ≤ f c<GOAL>b ≤ a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>s : Set α<GOAL>lowerBounds (closure s) = lowerBounds s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>s : Set α<GOAL>BddBelow (closure s) ↔ BddBelow s
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>Disjoint (𝓝 a) Filter.atTop ↔ ¬IsTop a
<VAR>α : Type u<VAR>Preorder α<VAR>NoTopOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>Disjoint (𝓝 a) Filter.atTop
<VAR>α : Type u<VAR>Preorder α<VAR>NoTopOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>𝓝 a ⊓ Filter.atTop = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>NoTopOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>l : Filter β<VAR>l.NeBot<VAR>f : β → α<VAR>hf : Filter.Tendsto f l Filter.atTop<VAR>a : α<GOAL>¬Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>NoTopOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>a : α<VAR>l : Filter β<VAR>l.NeBot<VAR>f : β → α<VAR>hf : Filter.Tendsto f l (𝓝 a)<GOAL>¬Filter.Tendsto f l Filter.atTop
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>IsOpen (Set.Iio a)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a : α<GOAL>interior (Set.Iio a) = Set.Iio a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Iio b ∈ 𝓝 a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>hab : a < b<GOAL>∀ᶠ (x : α) in 𝓝 a, x < b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a < b<GOAL>Set.Iic b ∈ 𝓝 a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>hab : a < b<GOAL>∀ᶠ (x : α) in 𝓝 a, x ≤ b
<VAR>α : Type u<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>l : Filter γ<VAR>f : γ → α<VAR>u v : α<VAR>hv : v < u<VAR>h : Filter.Tendsto f l (𝓝 v)<GOAL>∀ᶠ (a : γ) in l, f a < u
<VAR>α : Type u<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>l : Filter γ<VAR>f : γ → α<VAR>u v : α<VAR>hv : v < u<VAR>h : Filter.Tendsto f l (𝓝 v)<GOAL>∀ᶠ (a : γ) in l, f a ≤ u
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>NoMinOrder α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>∃ y ∈ s, y < x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>NoMinOrder α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<GOAL>∃ y ∈ s, y ≤ x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>s : Set α<VAR>hs : Dense s<VAR>hbot : ∀ (x : α), IsBot x → x ∈ s<VAR>x : α<GOAL>∃ y ∈ s, y ≤ x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ico a c<GOAL>Set.Ioo a c ∈ 𝓝[>] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ioo a b ∈ 𝓝[>] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a ⋖ b<GOAL>𝓝[>] a = ⊥
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ico a c<GOAL>Set.Ioc a c ∈ 𝓝[>] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ioc a b ∈ 𝓝[>] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ico a c<GOAL>Set.Ico a c ∈ 𝓝[>] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ico a b ∈ 𝓝[>] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ico a c<GOAL>Set.Icc a c ∈ 𝓝[>] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Icc a b ∈ 𝓝[>] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Ioc a b] a = 𝓝[>] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Ioo a b] a = 𝓝[>] a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Ioc a b) a ↔ ContinuousWithinAt f (Set.Ioi a) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Ioo a b) a ↔ ContinuousWithinAt f (Set.Ioi a) a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Ico a b ∈ 𝓝[≥] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ico a c<GOAL>Set.Ico a c ∈ 𝓝[≥] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioo a c<GOAL>Set.Ioo a c ∈ 𝓝[≥] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ioo a c<GOAL>Set.Ioc a c ∈ 𝓝[≥] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b c : α<VAR>H : b ∈ Set.Ico a c<GOAL>Set.Icc a c ∈ 𝓝[≥] b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>H : a < b<GOAL>Set.Icc a b ∈ 𝓝[≥] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Icc a b] a = 𝓝[≥] a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>a b : α<VAR>h : a < b<GOAL>𝓝[Set.Ico a b] a = 𝓝[≥] a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Icc a b) a ↔ ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>ClosedIciTopology α<VAR>TopologicalSpace β<VAR>a b : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Set.Ico a b) a ↔ ContinuousWithinAt f (Set.Ici a) a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<GOAL>IsClosed {p | p.1 ≤ p.2}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>IsClosed {b | f b ≤ g b}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>a b : α<GOAL>IsClosed (Set.Icc a b)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>a b : α<GOAL>closure (Set.Icc a b) = Set.Icc a b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>f g : β → α<VAR>b : Filter β<VAR>a₁ a₂ : α<VAR>b.NeBot<VAR>hf : Filter.Tendsto f b (𝓝 a₁)<VAR>hg : Filter.Tendsto g b (𝓝 a₂)<VAR>h : f ≤ᶠ[b] g<GOAL>a₁ ≤ a₂
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>f g : β → α<VAR>b : Filter β<VAR>a₁ a₂ : α<VAR>b.NeBot<VAR>hf : Filter.Tendsto f b (𝓝 a₁)<VAR>hg : Filter.Tendsto g b (𝓝 a₂)<VAR>h : ∀ (x : β), f x ≤ g x<GOAL>a₁ ≤ a₂
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>closure {b | f b ≤ g b} = {b | f b ≤ g b}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>closure {b | f b < g b} ⊆ {b | f b ≤ g b}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>s : Set β<VAR>x : β<VAR>hx : x ∈ closure s<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<VAR>h : ∀ y ∈ s, f y ≤ g y<GOAL>f x ≤ g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>s : Set β<VAR>hs : IsClosed s<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>IsClosed {x | x ∈ s ∧ f x ≤ g x}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>s : Set β<VAR>h : ∀ x ∈ s, f x ≤ g x<VAR>hf : ContinuousOn f (closure s)<VAR>hg : ContinuousOn g (closure s)<VAR>x : β<VAR>hx : x ∈ closure s<GOAL>f x ≤ g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<VAR>hs : IsClosed s<VAR>hf : ContinuousOn f s<GOAL>IsClosed {p | p.1 ∈ s ∧ f p.1 ≤ p.2}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder α<VAR>t : OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<VAR>hs : IsClosed s<VAR>hf : ContinuousOn f s<GOAL>IsClosed {p | p.1 ∈ s ∧ p.2 ≤ f p.1}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>IsOpen {b | f b < g b}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<GOAL>IsOpen {p | p.1 < p.2}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>IsOpen (Set.Ioo a b)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>interior (Set.Ioo a b) = Set.Ioo a b
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b : α<GOAL>Set.Ioo a b ⊆ closure (interior (Set.Ioo a b))
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b x : α<VAR>ha : a < x<VAR>hb : x < b<GOAL>Set.Ioo a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b x : α<VAR>ha : a < x<VAR>hb : x < b<GOAL>Set.Ioc a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b x : α<VAR>ha : a < x<VAR>hb : x < b<GOAL>Set.Ico a b ∈ 𝓝 x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a b x : α<VAR>ha : a < x<VAR>hb : x < b<GOAL>Set.Icc a b ∈ 𝓝 x
<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>{b | f b < g b} ⊆ interior {b | 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>frontier {b | f b ≤ g b} ⊆ {b | f b = g b}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>frontier (Set.Iic a) ⊆ {a}
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>a : α<GOAL>frontier (Set.Ici a) ⊆ {a}
<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>frontier {b | f b < g b} ⊆ {b | f b = g b}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>(x : β) → Decidable (f x ≤ g x)<VAR>f' g' : β → γ<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hf' : ContinuousOn f' {x | f x ≤ g x}<VAR>hg' : ContinuousOn g' {x | g x ≤ f x}<VAR>hfg : ∀ (x : β), f x = g x → f' x = g' x<GOAL>Continuous fun x => if f x ≤ g x then f' x else g' x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>(x : β) → Decidable (f x ≤ g x)<VAR>f' g' : β → γ<VAR>hf' : Continuous f'<VAR>hg' : Continuous g'<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hfg : ∀ (x : β), f x = g x → f' x = g' x<GOAL>Continuous fun x => if f x ≤ g x then f' x else g' x
<VAR>α : Type u<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>l : Filter γ<VAR>f g : γ → α<VAR>y z : α<VAR>hf : Filter.Tendsto f l (𝓝 y)<VAR>hg : Filter.Tendsto g l (𝓝 z)<VAR>hyz : y < z<GOAL>∀ᶠ (x : γ) in l, f x < g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderClosedTopology α<VAR>f g : β → α<VAR>TopologicalSpace β<VAR>x₀ : β<VAR>hf : ContinuousAt f x₀<VAR>hg : ContinuousAt g x₀<VAR>hfg : f x₀ < g x₀<GOAL>∀ᶠ (x : β) in 𝓝 x₀, f x < g x