ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b₁ b₂ c₁ c₂ d : R<GOAL>a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b : R<GOAL>0 * b = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₁ a₂ b c₁ c₂ d : R<GOAL>a₁ * b = c₁ → a₂ * b = c₂ → c₁ + c₂ = d → (a₁ + a₂) * b = d
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>n : ℕ<GOAL>↑n.rawCast = n.rawCast
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b₁ b₃ : R<VAR>a₁ a₃ : ℕ<VAR>a₂ : ℕ<GOAL>↑a₁ = b₁ → ↑a₃ = b₃ → ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b₁ b₂ : R<VAR>a₁ a₂ : ℕ<GOAL>↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂
<VAR>a b c : ℕ<GOAL>a * b = c → a • b = c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a' b c : R<VAR>a : ℕ<GOAL>↑a = a' → a' * b = c → a • b = c
<VAR>R : Type u_2<VAR>Ring R<VAR>a b : R<GOAL>(Int.negOfNat 1).rawCast * a = b → -a = b
<VAR>R : Type u_2<VAR>Ring R<VAR>a₁ : R<VAR>a₂ : ℕ<VAR>a₃ b : R<GOAL>-a₃ = b → -(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
<VAR>R : Type u_2<VAR>Ring R<GOAL>-0 = 0
<VAR>R : Type u_2<VAR>Ring R<VAR>a₁ a₂ b₁ b₂ : R<GOAL>-a₁ = b₁ → -a₂ = b₂ → -(a₁ + a₂) = b₁ + b₂
<VAR>R : Type u_2<VAR>Ring R<VAR>a b c d : R<GOAL>-b = c → a + c = d → a - b = d
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<VAR>b : ℕ<GOAL>a ^ b = (a + 0) ^ b * Nat.rawCast 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<VAR>b : ℕ<GOAL>a ^ b = a ^ b * Nat.rawCast 1 + 0
<VAR>n : ℕ<VAR>h : Nat.ble 1 n = true<GOAL>0 < n.rawCast
<VAR>a₁ a₂ : ℕ<VAR>n : ℕ<VAR>h₁ : 0 < a₁<VAR>h₂ : 0 < a₂<GOAL>0 < a₁ ^ n * a₂
<VAR>a₁ : ℕ<VAR>a₂ : ℕ<VAR>h : 0 < a₁<GOAL>0 < a₁ + a₂
<VAR>a₂ : ℕ<VAR>a₁ : ℕ<VAR>h : 0 < a₂<GOAL>0 < a₁ + a₂
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a ^ 1 = a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c : R<VAR>k : ℕ<GOAL>a ^ k = b → b * b = c → a ^ Nat.mul 2 k = c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b c : R<VAR>k : ℕ<VAR>d : R<GOAL>a ^ k = b → b * b = c → c * a = d → a ^ (Nat.mul 2 k).add 1 = d
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b : ℕ<GOAL>Nat.rawCast 1 ^ b = Nat.rawCast 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a₂ c₂ : R<VAR>ea₁ b c₁ : ℕ<VAR>xa₁ : R<GOAL>ea₁ * b = c₁ → a₂ ^ b = c₂ → (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂
<VAR>k : ℕ<GOAL>k.rawCast = Nat.rawCast 1 * k
<VAR>a₃ c₂ k : ℕ<VAR>a₁ a₂ : ℕ<GOAL>a₃ = c₂ * k → a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a ^ Nat.rawCast 1 = a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b : ℕ<GOAL>0 < b → 0 ^ b = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a c : R<VAR>b : ℕ<GOAL>a ^ b = c → (a + 0) ^ b = c + 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<VAR>b c k : ℕ<VAR>d e : R<GOAL>b = c * k → a ^ c = d → d ^ k = e → a ^ b = e
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a ^ 0 = Nat.rawCast 1 + 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a c₁ c₂ : R<VAR>b₁ b₂ : ℕ<VAR>d : R<GOAL>a ^ b₁ = c₁ → a ^ b₂ = c₂ → c₁ * c₂ = d → a ^ (b₁ + b₂) = d
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<VAR>n : ℕ<GOAL>Mathlib.Meta.NormNum.IsNat a n → a = n.rawCast + 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>Mathlib.Meta.NormNum.IsNat a 0 → a = 0
<VAR>n : ℕ<VAR>R : Type u_2<VAR>Ring R<VAR>a : R<GOAL>Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → a = (Int.negOfNat n).rawCast + 0
<VAR>n : ℤ<VAR>d : ℕ<VAR>R : Type u_2<VAR>DivisionRing R<VAR>a : R<GOAL>Mathlib.Meta.NormNum.IsRat a n d → a = Rat.rawCast n d + 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a a' : R<VAR>p : a = a'<GOAL>a = a' ^ Nat.rawCast 1 * Nat.rawCast 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>a = a ^ Nat.rawCast 1 * Nat.rawCast 1 + 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a a' : R<VAR>p : a = a'<GOAL>a = a' ^ Nat.rawCast 1 * Nat.rawCast 1 + 0
<VAR>R : Type u_2<VAR>DivisionRing R<VAR>a₁ : R<VAR>a₂ : ℕ<VAR>a₃ b₁ b₃ c : R<GOAL>a₁⁻¹ = b₁ → a₃⁻¹ = b₃ → b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c → (a₁ ^ a₂ * a₃)⁻¹ = c
<VAR>R : Type u_2<VAR>DivisionRing R<GOAL>0⁻¹ = 0
<VAR>R : Type u_2<VAR>DivisionRing R<VAR>a b : R<GOAL>a⁻¹ = b → (a + 0)⁻¹ = b + 0
<VAR>R : Type u_2<VAR>DivisionRing R<VAR>a b c d : R<GOAL>b⁻¹ = c → a * c = d → a / b = d
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a a' b b' c : R<GOAL>a = a' → b = b' → a' + b' = c → a + b = c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a a' b b' c : R<GOAL>a = a' → b = b' → a' * b' = c → a * b = c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>b b' c : R<VAR>a a' : ℕ<GOAL>a = a' → b = b' → a' • b' = c → a • b = c
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a a' c : R<VAR>b b' : ℕ<GOAL>a = a' → b = b' → a' ^ b' = c → a ^ b = c
<VAR>R : Type u_2<VAR>Ring R<VAR>a a' b : R<GOAL>a = a' → -a' = b → -a = b
<VAR>R : Type u_2<VAR>Ring R<VAR>a a' b b' c : R<GOAL>a = a' → b = b' → a' - b' = c → a - b = c
<VAR>R : Type u_2<VAR>DivisionRing R<VAR>a a' b : R<GOAL>a = a' → a'⁻¹ = b → a⁻¹ = b
<VAR>R : Type u_2<VAR>DivisionRing R<VAR>a a' b b' c : R<GOAL>a = a' → b = b' → a' / b' = c → a / b = c
<VAR>α : Type u<VAR>β : outParam (Type u)<VAR>self : Mathlib.Tactic.Ring.CSLift α β<GOAL>Function.Injective Mathlib.Tactic.Ring.CSLift.lift
<VAR>α : Type u<VAR>β : outParam (Type u)<VAR>Mathlib.Tactic.Ring.CSLift α β<VAR>a : α<VAR>b : outParam β<VAR>self : Mathlib.Tactic.Ring.CSLiftVal a b<GOAL>b = Mathlib.Tactic.Ring.CSLift.lift a
<VAR>α β : Type u_2<VAR>inst : Mathlib.Tactic.Ring.CSLift α β<VAR>a b : α<VAR>a' b' : β<VAR>h1 : Mathlib.Tactic.Ring.CSLiftVal a a'<VAR>h2 : Mathlib.Tactic.Ring.CSLiftVal b b'<VAR>h : a' = b'<GOAL>a = b
<VAR>α : Sort u_2<VAR>a b c : α<GOAL>a = c → b = c → a = b
<VAR>x y : ℕ<GOAL>dist x y = |↑x - ↑y|
<VAR>x : ℕ<VAR>r : ℝ<GOAL>Nat.cast ⁻¹' Metric.ball (↑x) r = Metric.ball x r
<VAR>x : ℕ<VAR>r : ℝ<GOAL>Nat.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
<VAR>x : ℕ<VAR>r : ℝ<GOAL>Metric.closedBall x r = Set.Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
<GOAL>preCantorSet 0 = Set.Icc 0 1
<VAR>n : ℕ<GOAL>preCantorSet (n + 1) = (fun x => x / 3) '' preCantorSet n ∪ (fun x => (2 + x) / 3) '' preCantorSet n
<VAR>n : ℕ<GOAL>1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
<VAR>n : ℕ<GOAL>1 / 4 ∈ preCantorSet n
<GOAL>cantorSet ⊆ Set.Icc 0 1
<VAR>n : ℕ<GOAL>IsClosed (preCantorSet n)
<VAR>x y : ℚ<GOAL>dist x y = |↑x - ↑y|
<VAR>x y : ℚ<GOAL>dist ↑x ↑y = dist x y
<VAR>a b : ℚ<GOAL>TotallyBounded (Set.Icc a b)
<GOAL>∀ᶠ (x : ℝ) in residual ℝ, Irrational x
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<GOAL>∀ᶠ (ε : ℝ) in 𝓝 0, ∀ k ≤ n, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
<VAR>x : ℝ<VAR>hx : Irrational x<VAR>n : ℕ<GOAL>∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (r : ℚ), r.den ≤ n → ε ≤ dist x ↑r
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>h : (Set.Ioi a).Nonempty<GOAL>closure (Set.Ioi a) = Set.Ici a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>NoMaxOrder α<GOAL>closure (Set.Ioi a) = Set.Ici a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>h : (Set.Iio a).Nonempty<GOAL>closure (Set.Iio a) = Set.Iic a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>NoMinOrder α<GOAL>closure (Set.Iio a) = Set.Iic a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Set.Ioo a b) = Set.Icc a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Set.Ioc a b) = Set.Icc a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>closure (Set.Ico a b) = Set.Icc a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>ha : (Set.Iio a).Nonempty<GOAL>interior (Set.Ici a) = Set.Ioi a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a : α<GOAL>interior (Set.Ici a) = Set.Ioi a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>ha : (Set.Ioi a).Nonempty<GOAL>interior (Set.Iic a) = Set.Iio a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a : α<GOAL>interior (Set.Iic a) = Set.Iio a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>interior (Set.Icc a b) = Set.Ioo a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>NoMaxOrder α<VAR>a b x : α<GOAL>Set.Icc a b ∈ 𝓝 x ↔ x ∈ Set.Ioo a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a b : α<GOAL>interior (Set.Ico a b) = Set.Ioo a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a b x : α<GOAL>Set.Ico a b ∈ 𝓝 x ↔ x ∈ Set.Ioo a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>interior (Set.Ioc a b) = Set.Ioo a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a b x : α<GOAL>Set.Ioc a b ∈ 𝓝 x ↔ x ∈ Set.Ioo a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a ≠ b<GOAL>closure (interior (Set.Icc a b)) = Set.Icc a b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>Set.Ioc a b ⊆ closure (interior (Set.Ioc a b))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>Set.Ico a b ⊆ closure (interior (Set.Ico a b))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>ha : (Set.Iio a).Nonempty<GOAL>frontier (Set.Ici a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a : α<GOAL>frontier (Set.Ici a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>ha : (Set.Ioi a).Nonempty<GOAL>frontier (Set.Iic a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a : α<GOAL>frontier (Set.Iic a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>ha : (Set.Ioi a).Nonempty<GOAL>frontier (Set.Ioi a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a : α<GOAL>frontier (Set.Ioi a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>ha : (Set.Iio a).Nonempty<GOAL>frontier (Set.Iio a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a : α<GOAL>frontier (Set.Iio a) = {a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>NoMaxOrder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>frontier (Set.Icc a b) = {a, b}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>frontier (Set.Ioo a b) = {a, b}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a b : α<VAR>h : a < b<GOAL>frontier (Set.Ico a b) = {a, b}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a b : α<VAR>h : a < b<GOAL>frontier (Set.Ioc a b) = {a, b}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>H₁ : (Set.Ioi a).Nonempty<VAR>H₂ : a ≤ b<GOAL>(𝓝[Set.Ioi a] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMaxOrder α<VAR>a b : α<VAR>H : a ≤ b<GOAL>(𝓝[Set.Ioi a] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>H : (Set.Ioi a).Nonempty<GOAL>(𝓝[>] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>b c : α<VAR>H₁ : (Set.Iio c).Nonempty<VAR>H₂ : b ≤ c<GOAL>(𝓝[Set.Iio c] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>NoMinOrder α<VAR>a b : α<VAR>H : a ≤ b<GOAL>(𝓝[Set.Iio b] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>b : α<VAR>H : (Set.Iio b).Nonempty<GOAL>(𝓝[<] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>H : a < b<GOAL>(𝓝[Set.Ico a b] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>H : a < b<GOAL>(𝓝[Set.Ioc a b] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>H : a < b<GOAL>(𝓝[Set.Ioo a b] a).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>H : a < b<GOAL>(𝓝[Set.Ioo a b] b).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>b : α<VAR>s : Set α<VAR>hb : s ⊆ Set.Iio b<VAR>hs : s.Nonempty → ∃ a < b, Set.Ioo a b ⊆ s<GOAL>Filter.comap Subtype.val (𝓝[<] b) = Filter.atTop
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>s : Set α<VAR>ha : s ⊆ Set.Ioi a<VAR>hs : s.Nonempty → ∃ b > a, Set.Ioo a b ⊆ s<GOAL>Filter.comap Subtype.val (𝓝[>] a) = Filter.atBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>b : α<VAR>s : Set α<VAR>hb : s ⊆ Set.Iio b<VAR>hs : ∀ a' < b, ∃ a < b, Set.Ioo a b ⊆ s<GOAL>Filter.map Subtype.val Filter.atTop = 𝓝[<] b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>s : Set α<VAR>ha : s ⊆ Set.Ioi a<VAR>hs : ∀ b' > a, ∃ b > a, Set.Ioo a b ⊆ s<GOAL>Filter.map Subtype.val Filter.atBot = 𝓝[>] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>Filter.comap Subtype.val (𝓝[<] b) = Filter.atTop
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<GOAL>Filter.comap Subtype.val (𝓝[>] a) = Filter.atBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>Filter.comap Subtype.val (𝓝[>] a) = Filter.atBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>Filter.comap Subtype.val (𝓝[<] a) = Filter.atTop
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>Filter.map Subtype.val Filter.atTop = 𝓝[<] b
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>h : a < b<GOAL>Filter.map Subtype.val Filter.atBot = 𝓝[>] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>Filter.map Subtype.val Filter.atBot = 𝓝[>] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<GOAL>Filter.map Subtype.val Filter.atTop = 𝓝[<] a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>l : Filter β<VAR>f : α → β<VAR>h : a < b<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (𝓝[<] b) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>l : Filter β<VAR>f : α → β<VAR>h : a < b<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (𝓝[>] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>l : Filter β<VAR>f : α → β<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atBot l ↔ Filter.Tendsto f (𝓝[>] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>l : Filter β<VAR>f : α → β<GOAL>Filter.Tendsto (fun x => f ↑x) Filter.atTop l ↔ Filter.Tendsto f (𝓝[<] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>l : Filter β<VAR>f : β → ↑(Set.Ioo a b)<GOAL>Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l (𝓝[<] b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a b : α<VAR>l : Filter β<VAR>f : β → ↑(Set.Ioo a b)<GOAL>Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>l : Filter β<VAR>f : β → ↑(Set.Ioi a)<GOAL>Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l (𝓝[>] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>a : α<VAR>l : Filter β<VAR>f : β → ↑(Set.Iio a)<GOAL>Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun x => ↑(f x)) l (𝓝[<] a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>Nontrivial α<VAR>s : Set α<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hs : Dense s<GOAL>∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>DenselyOrdered α<VAR>TopologicalSpace.SeparableSpace α<VAR>Nontrivial α<GOAL>∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∉ s) ∧ ∀ (x : α), IsTop x → x ∉ s
<VAR>x y : ℕ+<GOAL>dist x y = |↑↑x - ↑↑y|
<VAR>x y : ℕ+<GOAL>dist ↑x ↑y = dist x y
<VAR>α : Type u_1<VAR>Zero α<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>OrderTopology α<VAR>a : α<VAR>h : 0 < a<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>Zero α<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>OrderTopology α<VAR>a : α<VAR>h : a < 0<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>Zero α<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>OrderTopology α<VAR>a : α<VAR>h : a ≠ 0<GOAL>ContinuousAt (⇑SignType.sign) a
<GOAL>⇑ContinuousMap.realToNNReal = Real.toNNReal
<GOAL>⇑ContinuousMap.coeNNRealReal = NNReal.toReal
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → NNReal<VAR>x : NNReal<GOAL>Filter.Tendsto (fun a => ↑(m a)) f (𝓝 ↑x) ↔ Filter.Tendsto m f (𝓝 x)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>f.NeBot<VAR>m : α → NNReal<VAR>x : ℝ<GOAL>Filter.Tendsto (fun a => ↑(m a)) f (𝓝 x) ↔ ∃ (hx : 0 ≤ x), Filter.Tendsto m f (𝓝 ⟨x, hx⟩)
<GOAL>Filter.map NNReal.toReal Filter.atTop = Filter.atTop
<GOAL>Filter.comap NNReal.toReal Filter.atTop = Filter.atTop
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → NNReal<GOAL>Filter.Tendsto (fun a => ↑(m a)) f Filter.atTop ↔ Filter.Tendsto m f Filter.atTop
<VAR>α : Type u_1<VAR>f : Filter α<VAR>m : α → ℝ<VAR>x : ℝ<VAR>h : Filter.Tendsto m f (𝓝 x)<GOAL>Filter.Tendsto (fun a => (m a).toNNReal) f (𝓝 x.toNNReal)
<GOAL>Filter.map Real.toNNReal Filter.atTop = Filter.atTop
<GOAL>Filter.Tendsto Real.toNNReal Filter.atTop Filter.atTop
<GOAL>Filter.comap Real.toNNReal Filter.atTop = Filter.atTop
<VAR>α : Type u_1<VAR>l : Filter α<VAR>f : α → ℝ<GOAL>Filter.Tendsto (fun x => (f x).toNNReal) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
<GOAL>𝓝 0 = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)
<GOAL>(𝓝 0).HasBasis (fun a => 0 < a) fun a => Set.Iio a
<VAR>α : Type u_1<VAR>f : α → NNReal<VAR>r : NNReal<GOAL>HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf_nonneg : ∀ (n : α), 0 ≤ f n<VAR>hf : Summable f<GOAL>HasSum (fun n => (f n).toNNReal) (∑' (n : α), f n).toNNReal
<VAR>α : Type u_1<VAR>f : α → NNReal<GOAL>(Summable fun a => ↑(f a)) ↔ Summable f
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf : ∀ (n : α), 0 ≤ f n<GOAL>(Summable fun n => ⟨f n, ⋯⟩) ↔ Summable f
<VAR>α : Type u_1<VAR>f : α → NNReal<GOAL>↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf₁ : ∀ (n : α), 0 ≤ f n<GOAL>⟨∑' (n : α), f n, ⋯⟩ = ∑' (n : α), ⟨f n, ⋯⟩
<VAR>α : Type u_1<VAR>a : NNReal<VAR>f : α → NNReal<GOAL>∑' (x : α), a * f x = a * ∑' (x : α), f x
<VAR>α : Type u_1<VAR>f : α → NNReal<VAR>a : NNReal<GOAL>∑' (x : α), f x * a = (∑' (x : α), f x) * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → NNReal<VAR>hf : Summable f<VAR>i : β → α<VAR>hi : Function.Injective i<GOAL>Summable (f ∘ i)
<VAR>f : ℕ → NNReal<VAR>hf : Summable f<VAR>k : ℕ<GOAL>Summable fun i => f (i + k)
<VAR>f : ℕ → NNReal<VAR>k : ℕ<GOAL>(Summable fun i => f (i + k)) ↔ Summable f
<VAR>f : ℕ → NNReal<VAR>k : ℕ<VAR>a : NNReal<GOAL>HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
<VAR>f : ℕ → NNReal<VAR>k : ℕ<VAR>hf : Summable f<GOAL>∑' (i : ℕ), f i = ∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>f : ℝ → α<GOAL>⨅ n, ⨅ (_ : 0 < n), f n = ⨅ n, ⨅ (_ : 0 < n), f ↑n
<VAR>α : Type u_1<VAR>f : α → NNReal<VAR>hf : Summable f<GOAL>Filter.Tendsto f Filter.cofinite (𝓝 0)
<VAR>f : ℕ → NNReal<VAR>hf : Summable f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 0)
<VAR>α : Type u_1<VAR>f : α → NNReal<GOAL>Filter.Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) Filter.atTop (𝓝 0)
<VAR>f : ℕ → ℝ<VAR>h_bdd : BddAbove (Set.range f)<VAR>h_mon : Monotone f<GOAL>∃ r, Filter.Tendsto f Filter.atTop (𝓝 r)
<VAR>f : ℕ → ℝ<VAR>h_bdd : BddBelow (Set.range f)<VAR>h_ant : Antitone f<GOAL>∃ r, Filter.Tendsto f Filter.atTop (𝓝 r)
<VAR>f : ℕ → NNReal<VAR>h_ant : Antitone f<GOAL>∃ r, Filter.Tendsto f Filter.atTop (𝓝 r)
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>Countable α<GOAL>SecondCountableTopology α
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>PredOrder α<VAR>SuccOrder α<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>⊥ = TopologicalSpace.generateFrom {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PartialOrder α<VAR>PredOrder α<VAR>SuccOrder α<VAR>NoMinOrder α<VAR>NoMaxOrder α<GOAL>DiscreteTopology α ↔ OrderTopology α
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>SuccOrder α<GOAL>⊥ = TopologicalSpace.generateFrom {s | ∃ a, s = Set.Ioi a ∨ s = Set.Iio a}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>PredOrder α<VAR>SuccOrder α<GOAL>DiscreteTopology α ↔ OrderTopology α
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>PreconnectedSpace X<VAR>a b : X<VAR>f g : X → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>ha : f a ≤ g a<VAR>hb : g b ≤ f b<GOAL>∃ x, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>PreconnectedSpace X<VAR>a : X<VAR>l : Filter X<VAR>l.NeBot<VAR>f g : X → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>ha : f a ≤ g a<VAR>he : g ≤ᶠ[l] f<GOAL>∃ x, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>PreconnectedSpace X<VAR>l₁ l₂ : Filter X<VAR>l₁.NeBot<VAR>l₂.NeBot<VAR>f g : X → α<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>he₁ : f ≤ᶠ[l₁] g<VAR>he₂ : g ≤ᶠ[l₂] f<GOAL>∃ x, f x = g x
<VAR>X : Type u<VAR>α : Type v<VAR>TopologicalSpace X<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>s : Set X<VAR>hs : IsPreconnected s<VAR>a b : X<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>f g : X → α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<VAR>ha' : f a ≤ g a<VAR>hb' : g b ≤ f b<GOAL>∃ x ∈ s, f x = g x