ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>a : Topology.WithUpper α<GOAL>Topology.WithUpper.toUpper (Topology.WithUpper.ofUpper a) = a
<VAR>α : Type u_1<VAR>a : α<GOAL>Topology.WithUpper.ofUpper (Topology.WithUpper.toUpper a) = a
<VAR>α : Type u_1<VAR>a b : α<GOAL>Topology.WithUpper.toUpper a = Topology.WithUpper.toUpper b ↔ a = b
<VAR>α : Type u_1<VAR>a b : Topology.WithUpper α<GOAL>Topology.WithUpper.ofUpper a = Topology.WithUpper.ofUpper b ↔ a = b
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>IsOpen (⇑Topology.WithUpper.ofUpper ⁻¹' s) ↔ TopologicalSpace.IsOpen s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set (Topology.WithUpper α)<GOAL>IsOpen s ↔ TopologicalSpace.IsOpen (⇑Topology.WithUpper.toUpper ⁻¹' s)
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<VAR>Preorder α<VAR>self : Topology.IsLower α<GOAL>t = Topology.lower α
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<VAR>Preorder α<VAR>self : Topology.IsUpper α<GOAL>t = Topology.upper α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<GOAL>inst✝ = Topology.lower α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>s : Set α<GOAL>IsOpen s ↔ TopologicalSpace.GenerateOpen {t | ∃ a, (Set.Ici a)ᶜ = t} s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>s : Set α<VAR>h : s.Finite<GOAL>IsClosed ↑(upperClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>s : Set α<VAR>h : IsOpen s<GOAL>IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>s : Set α<VAR>h : IsClosed s<GOAL>IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>a : α<GOAL>closure {a} = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<GOAL>TopologicalSpace.IsTopologicalBasis (Topology.IsLower.lowerBasis α)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<GOAL>inst✝ = Topology.upper α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>s : Set α<GOAL>IsOpen s ↔ TopologicalSpace.GenerateOpen {t | ∃ a, (Set.Iic a)ᶜ = t} s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>s : Set α<VAR>h : s.Finite<GOAL>IsClosed ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>s : Set α<VAR>h : IsOpen s<GOAL>IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>s : Set α<VAR>h : IsClosed s<GOAL>IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>a : α<GOAL>closure {a} = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<GOAL>TopologicalSpace.IsTopologicalBasis (Topology.IsUpper.upperBasis α)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>h : ∀ (a : α), IsClosed (f ⁻¹' Set.Iic a)<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>TopologicalSpace α<VAR>Topology.IsLower α<VAR>TopologicalSpace β<VAR>Topology.IsLower β<VAR>f : sInfHom α β<GOAL>Continuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>TopologicalSpace α<VAR>Topology.IsUpper α<VAR>TopologicalSpace β<VAR>Topology.IsUpper β<VAR>f : sSupHom α β<GOAL>Continuous ⇑f
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<GOAL>Topology.IsUpper αᵒᵈ ↔ Topology.IsLower α
<VAR>α : Type u_1<VAR>Preorder α<VAR>TopologicalSpace α<GOAL>Topology.IsLower αᵒᵈ ↔ Topology.IsUpper α
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<GOAL>Absorbs M s ∅
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t : Set α<VAR>h : Absorbs M s t<GOAL>∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t : Set α<VAR>BoundedSpace M<GOAL>Absorbs M s t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s₁ s₂ t : Set α<VAR>h : Absorbs M s₁ t<VAR>hs : s₁ ⊆ s₂<GOAL>Absorbs M s₂ t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t₁ t₂ : Set α<VAR>h : Absorbs M s t₁<VAR>ht : t₂ ⊆ t₁<GOAL>Absorbs M s t₂
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s₁ s₂ t₁ t₂ : Set α<VAR>h : Absorbs M s₁ t₁<VAR>hs : s₁ ⊆ s₂<VAR>ht : t₂ ⊆ t₁<GOAL>Absorbs M s₂ t₂
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t₁ t₂ : Set α<GOAL>Absorbs M s (t₁ ∪ t₂) ↔ Absorbs M s t₁ ∧ Absorbs M s t₂
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t₁ t₂ : Set α<VAR>h₁ : Absorbs M s t₁<VAR>h₂ : Absorbs M s t₂<GOAL>Absorbs M s (t₁ ∪ t₂)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<VAR>T : Set (Set α)<VAR>hT : T.Finite<GOAL>Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<VAR>T : Set (Set α)<VAR>hT : T.Finite<VAR>hs : ∀ t ∈ T, Absorbs M s t<GOAL>Absorbs M s (⋃₀ T)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>Finite ι<VAR>t : ι → Set α<GOAL>Absorbs M s (⋃ i, t i) ↔ ∀ (i : ι), Absorbs M s (t i)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<VAR>ι : Type u_3<VAR>t : ι → Set α<VAR>I : Set ι<VAR>hI : I.Finite<GOAL>Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<VAR>ι : Type u_3<VAR>t : ι → Set α<VAR>I : Finset ι<GOAL>Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>Bornology M<VAR>s₁ s₂ t₁ t₂ : Set E<VAR>AddZeroClass E<VAR>DistribSMul M E<VAR>h₁ : Absorbs M s₁ t₁<VAR>h₂ : Absorbs M s₂ t₂<GOAL>Absorbs M (s₁ + s₂) (t₁ + t₂)
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>Bornology M<VAR>Zero E<VAR>SMulZeroClass M E<VAR>s : Set E<VAR>hs : 0 ∈ s<GOAL>Absorbs M s 0
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>s : Set α<GOAL>Absorbs G₀ Set.univ s
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>s t : Set α<GOAL>Absorbs G₀ s t ↔ ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun x => c⁻¹ • x) t s
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>t : Set α<VAR>S : Set (Set α)<VAR>hS : S.Finite<GOAL>Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>s t u : Set α<GOAL>Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>s t u : Set α<VAR>hs : Absorbs G₀ s u<VAR>ht : Absorbs G₀ t u<GOAL>Absorbs G₀ (s ∩ t) u
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>t : Set α<VAR>ι : Sort u_3<VAR>Finite ι<VAR>s : ι → Set α<GOAL>Absorbs G₀ (⋂ i, s i) t ↔ ∀ (i : ι), Absorbs G₀ (s i) t
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>t : Set α<VAR>ι : Type u_3<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set α<GOAL>Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t
<VAR>G₀ : Type u_1<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>(Bornology.cobounded G₀).NeBot<VAR>E : Type u_3<VAR>AddMonoid E<VAR>DistribMulAction G₀ E<VAR>s : Set E<GOAL>Absorbs G₀ s 0 ↔ 0 ∈ s
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>Monoid M<VAR>AddGroup E<VAR>DistribMulAction M E<VAR>Bornology M<VAR>s t : Set E<GOAL>Absorbs M (-s) (-t) ↔ Absorbs M s t
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>Monoid M<VAR>AddGroup E<VAR>DistribMulAction M E<VAR>Bornology M<VAR>s₁ s₂ t₁ t₂ : Set E<VAR>h₁ : Absorbs M s₁ t₁<VAR>h₂ : Absorbs M s₂ t₂<GOAL>Absorbs M (s₁ - s₂) (t₁ - t₂)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t : Set α<VAR>ht : Absorbent M s<VAR>hsub : s ⊆ t<GOAL>Absorbent M t
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<GOAL>Absorbent M s ↔ ∀ (x : α), Absorbs M s {x}
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s : Set α<VAR>hs : Absorbent M s<VAR>x : α<GOAL>Absorbs M s {x}
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>Bornology M<VAR>SMul M α<VAR>s t : Set α<VAR>hs : Absorbent M s<VAR>ht : t.Finite<GOAL>Absorbs M s t
<VAR>M : Type u_1<VAR>E : Type u_2<VAR>Bornology M<VAR>AddZeroClass E<VAR>DistribSMul M E<VAR>s₁ s₂ t : Set E<VAR>x : E<VAR>h₁ : Absorbent M s₁<VAR>h₂ : Absorbs M s₂ t<GOAL>Absorbs M (s₁ + s₂) (x +ᵥ t)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<GOAL>Absorbent G₀ Set.univ
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>MulAction G₀ α<VAR>s : Set α<GOAL>Absorbent G₀ s ↔ ∀ (x : α), ∀ᶠ (c : G₀) in Bornology.cobounded G₀, c⁻¹ • x ∈ s
<VAR>G₀ : Type u_1<VAR>E : Type u_3<VAR>GroupWithZero G₀<VAR>Bornology G₀<VAR>(Bornology.cobounded G₀).NeBot<VAR>AddMonoid E<VAR>DistribMulAction G₀ E<VAR>s : Set E<VAR>hs : Absorbent G₀ s<GOAL>0 ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace β<VAR>hα : TopologicalSpace α<VAR>h'α : OrderTopology α<VAR>T2Space β<VAR>f : α → β<VAR>a : α<VAR>y : β<VAR>h : 𝓝[<] a ≠ ⊥<VAR>h' : Filter.Tendsto f (𝓝[<] a) (𝓝 y)<GOAL>Function.leftLim f a = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace β<VAR>hα : TopologicalSpace α<VAR>h'α : OrderTopology α<VAR>f : α → β<VAR>a : α<VAR>h : 𝓝[<] a = ⊥<GOAL>Function.leftLim f a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace β<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>T2Space β<VAR>f : α → β<VAR>a : α<VAR>y : β<VAR>h : 𝓝[>] a ≠ ⊥<VAR>h' : Filter.Tendsto f (𝓝[>] a) (𝓝 y)<GOAL>Function.rightLim f a = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>TopologicalSpace β<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>f : α → β<VAR>a : α<VAR>h : 𝓝[>] a = ⊥<GOAL>Function.rightLim f a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>h : 𝓝[<] x ≠ ⊥<GOAL>Function.leftLim f x = sSup (f '' Set.Iio x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>h : 𝓝[>] x ≠ ⊥<GOAL>Function.rightLim f x = sInf (f '' Set.Ioi x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<GOAL>Function.leftLim f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<GOAL>f x ≤ Function.leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Monotone (Function.leftLim f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<GOAL>f x ≤ Function.rightLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<GOAL>Function.rightLim f x ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Monotone (Function.rightLim f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x ≤ y<GOAL>Function.leftLim f x ≤ Function.rightLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>h : x < y<GOAL>Function.rightLim f x ≤ Function.leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[<] x) (𝓝 (Function.leftLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[<] x) (𝓝[≤] Function.leftLim f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[>] x) (𝓝 (Function.rightLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[>] x) (𝓝[≥] Function.rightLim f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>SecondCountableTopology β<GOAL>{x | ¬ContinuousWithinAt f (Set.Ioi x) x}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>SecondCountableTopology β<GOAL>{x | ¬ContinuousWithinAt f (Set.Iio x) x}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>SecondCountableTopology β<GOAL>{x | ¬ContinuousAt f x}.Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<VAR>h : x ≤ y<GOAL>f y ≤ Function.leftLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<VAR>h : x < y<GOAL>Function.leftLim f y ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Antitone (Function.leftLim f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<VAR>h : x ≤ y<GOAL>Function.rightLim f y ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<VAR>h : x < y<GOAL>f y ≤ Function.rightLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<GOAL>Antitone (Function.rightLim f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<VAR>h : x ≤ y<GOAL>Function.rightLim f y ≤ Function.leftLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x y : α<VAR>h : x < y<GOAL>Function.leftLim f y ≤ Function.rightLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[<] x) (𝓝 (Function.leftLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[<] x) (𝓝[≥] Function.leftLim f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[>] x) (𝓝 (Function.rightLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>x : α<GOAL>Filter.Tendsto f (𝓝[>] x) (𝓝[≤] Function.rightLim f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>ContinuousWithinAt f (Set.Iio x) x ↔ Function.leftLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>ContinuousWithinAt f (Set.Ioi x) x ↔ Function.rightLim f x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>x : α<VAR>TopologicalSpace α<VAR>OrderTopology α<GOAL>ContinuousAt f x ↔ Function.leftLim f x = Function.rightLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>ConditionallyCompleteLinearOrder β<VAR>TopologicalSpace β<VAR>OrderTopology β<VAR>f : α → β<VAR>hf : Antitone f<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>SecondCountableTopology β<GOAL>{x | ¬ContinuousAt f x}.Countable
<VAR>α : Type u_4<VAR>TopologicalSpace α<VAR>self : TopologicalSpace.Closeds α<GOAL>IsClosed self.carrier
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>IsClosed ↑s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Closeds α<VAR>h : ↑s = ↑t<GOAL>s = t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>h : IsClosed s<GOAL>↑{ carrier := s, closed' := h } = s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>↑(TopologicalSpace.Closeds.closure s) = closure s
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>GaloisConnection TopologicalSpace.Closeds.closure SetLike.coe
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Closeds α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s t : TopologicalSpace.Closeds α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>↑s = Set.univ ↔ s = ⊤
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>↑⊥ = ∅
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>↑s = ∅ ↔ s = ⊥
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>(↑s).Nonempty ↔ s ≠ ⊥
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>S : Set (TopologicalSpace.Closeds α)<GOAL>↑(sInf S) = ⋂ i ∈ S, ↑i
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>S : Set (TopologicalSpace.Closeds α)<GOAL>↑(sSup S) = closure (⋃₀ (SetLike.coe '' S))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : ι → TopologicalSpace.Closeds α<VAR>s : Finset ι<GOAL>↑(s.sup f) = s.sup (SetLike.coe ∘ f)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : ι → TopologicalSpace.Closeds α<VAR>s : Finset ι<GOAL>↑(s.inf f) = s.inf (SetLike.coe ∘ f)
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>S : Set (TopologicalSpace.Closeds α)<VAR>x : α<GOAL>x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_4<VAR>x : α<VAR>s : ι → TopologicalSpace.Closeds α<GOAL>x ∈ iInf s ↔ ∀ (i : ι), x ∈ s i
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_4<VAR>s : ι → TopologicalSpace.Closeds α<GOAL>↑(⨅ i, s i) = ⋂ i, ↑(s i)
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_4<VAR>s : ι → TopologicalSpace.Closeds α<GOAL>⨅ i, s i = { carrier := ⋂ i, ↑(s i), closed' := ⋯ }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>ι : Sort u_4<VAR>s : ι → Set α<VAR>h : ∀ (i : ι), IsClosed (s i)<GOAL>⨅ i, { carrier := s i, closed' := ⋯ } = { carrier := ⋂ i, s i, closed' := ⋯ }
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>x : α<GOAL>↑(TopologicalSpace.Closeds.singleton x) = {x}
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>a b : α<GOAL>a ∈ TopologicalSpace.Closeds.singleton b ↔ a = b
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>↑s.compl = (↑s)ᶜ
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Opens α<GOAL>↑s.compl = (↑s)ᶜ
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>s.compl.compl = s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>s : TopologicalSpace.Opens α<GOAL>s.compl.compl = s
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>Function.Bijective TopologicalSpace.Closeds.compl
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>Function.Bijective TopologicalSpace.Opens.compl
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>∀ (a : TopologicalSpace.Closeds α), (TopologicalSpace.Closeds.complOrderIso α) a = (⇑OrderDual.toDual ∘ TopologicalSpace.Closeds.compl) a
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>∀ (a : (TopologicalSpace.Opens α)ᵒᵈ), (RelIso.symm (TopologicalSpace.Closeds.complOrderIso α)) a = (TopologicalSpace.Opens.compl ∘ ⇑OrderDual.ofDual) a
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>∀ (a : (TopologicalSpace.Closeds α)ᵒᵈ), (RelIso.symm (TopologicalSpace.Opens.complOrderIso α)) a = (TopologicalSpace.Closeds.compl ∘ ⇑OrderDual.ofDual) a
<VAR>α : Type u_2<VAR>TopologicalSpace α<GOAL>∀ (a : TopologicalSpace.Opens α), (TopologicalSpace.Opens.complOrderIso α) a = (⇑OrderDual.toDual ∘ TopologicalSpace.Opens.compl) a
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T0Space α<VAR>s : TopologicalSpace.Closeds α<VAR>hs : IsAtom s<GOAL>∃ a, ↑s = {a}
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>s : TopologicalSpace.Closeds α<GOAL>IsAtom ↑s ↔ IsAtom s
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>T1Space α<VAR>s : TopologicalSpace.Closeds α<GOAL>IsAtom s ↔ ∃ x, s = TopologicalSpace.Closeds.singleton x