ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>γ : Type u_3<VAR>F : β → γ → α<VAR>s : Set γ<GOAL>UniformCauchySeqOn F Filter.atTop s ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>s : β → α<VAR>b : β → ℝ<VAR>h : ∀ (n m : β), n ≤ m → dist (s n) (s m) ≤ b n<VAR>h₀ : Filter.Tendsto b Filter.atTop (𝓝 0)<GOAL>CauchySeq s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>s : β → α<VAR>b : β → ℝ<VAR>h : ∀ (n m N : β), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N<VAR>h₀ : Filter.Tendsto b Filter.atTop (𝓝 0)<GOAL>CauchySeq s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : ℕ → α<GOAL>CauchySeq s ↔ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (𝓝 0)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>b : ℕ → ℝ<VAR>hb : ∀ (n : ℕ), 0 < b n<GOAL>∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>x : ↑(CantorScheme.inducedMap A).fst<VAR>n : ℕ<GOAL>(CantorScheme.inducedMap A).snd x ∈ A (PiNat.res (↑x) n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>TopologicalSpace α<VAR>hA : CantorScheme.ClosureAntitone A<GOAL>CantorScheme.Antitone A
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>TopologicalSpace α<VAR>hanti : CantorScheme.Antitone A<VAR>hclosed : ∀ (l : List β), IsClosed (A l)<GOAL>CantorScheme.ClosureAntitone A
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>hA : CantorScheme.Disjoint A<GOAL>Function.Injective (CantorScheme.inducedMap A).snd
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>PseudoMetricSpace α<VAR>hA : CantorScheme.VanishingDiam A<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>x : ℕ → β<GOAL>∃ n, ∀ y ∈ A (PiNat.res x n), ∀ z ∈ A (PiNat.res x n), dist y z < ε
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>DiscreteTopology β<VAR>hA : CantorScheme.VanishingDiam A<GOAL>Continuous (CantorScheme.inducedMap A).snd
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>PseudoMetricSpace α<VAR>CompleteSpace α<VAR>hdiam : CantorScheme.VanishingDiam A<VAR>hanti : CantorScheme.ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<GOAL>(CantorScheme.inducedMap A).fst = Set.univ
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>self : LipschitzAdd β<GOAL>∃ C, LipschitzWith C fun p => p.1 + p.2
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>Monoid β<VAR>self : LipschitzMul β<GOAL>∃ C, LipschitzWith C fun p => p.1 * p.2
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>Monoid β<VAR>_i : LipschitzMul β<GOAL>LipschitzWith (LipschitzMul.C β) fun p => p.1 * p.2
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>_i : LipschitzAdd β<GOAL>LipschitzWith (LipschitzAdd.C β) fun p => p.1 + p.2
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>Monoid β<VAR>LipschitzMul β<VAR>p q : β × β<GOAL>dist (p.1 * p.2) (q.1 * q.2) ≤ ↑(LipschitzMul.C β) * dist p q
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>LipschitzAdd β<VAR>p q : β × β<GOAL>dist (p.1 + p.2) (q.1 + q.2) ≤ ↑(LipschitzAdd.C β) * dist p q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>Zero α<VAR>Zero β<VAR>SMul α β<VAR>self : BoundedSMul α β<VAR>x : α<VAR>y₁ y₂ : β<GOAL>dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>Zero α<VAR>Zero β<VAR>SMul α β<VAR>self : BoundedSMul α β<VAR>x₁ x₂ : α<VAR>y : β<GOAL>dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>Zero α<VAR>Zero β<VAR>SMul α β<VAR>BoundedSMul α β<VAR>x : α<VAR>y₁ y₂ : β<GOAL>dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>Zero α<VAR>Zero β<VAR>SMul α β<VAR>BoundedSMul α β<VAR>x₁ x₂ : α<VAR>y : β<GOAL>dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
<VAR>α : Type u<VAR>n : ℕ<VAR>MetricSpace α<VAR>x : ℕ → α<VAR>a : α<GOAL>↑(KuratowskiEmbedding.embeddingOfSubset x a) n = dist a (x n) - dist (x 0) (x n)
<VAR>α : Type u<VAR>MetricSpace α<VAR>x : ℕ → α<VAR>a b : α<GOAL>dist (KuratowskiEmbedding.embeddingOfSubset x a) (KuratowskiEmbedding.embeddingOfSubset x b) ≤ dist a b
<VAR>α : Type u<VAR>MetricSpace α<VAR>x : ℕ → α<VAR>H : DenseRange x<GOAL>Isometry (KuratowskiEmbedding.embeddingOfSubset x)
<VAR>α : Type u<VAR>MetricSpace α<VAR>TopologicalSpace.SeparableSpace α<GOAL>∃ f, Isometry f
<VAR>α : Type u<VAR>MetricSpace α<VAR>TopologicalSpace.SeparableSpace α<GOAL>Isometry (kuratowskiEmbedding α)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ι : Type u_1<VAR>f : α → ↥(lp (fun i => ℝ) ⊤)<VAR>K : ℝ≥0<VAR>hfl : LipschitzOnWith K f s<GOAL>∃ g, LipschitzWith K g ∧ Set.EqOn f g s
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>UniformContinuous fun p => dist p.1 p.2
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f g : β → UniformSpace.Completion α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => dist (f x) (g x)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>dist (↑α x) (↑α y) = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : UniformSpace.Completion α<GOAL>dist x x = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : UniformSpace.Completion α<GOAL>dist x y = dist y x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : UniformSpace.Completion α<GOAL>dist x z ≤ dist x y + dist y z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set (UniformSpace.Completion α × UniformSpace.Completion α)<GOAL>s ∈ 𝓤 (UniformSpace.Completion α) ↔ ∃ ε > 0, ∀ {a b : UniformSpace.Completion α}, dist a b < ε → (a, b) ∈ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>𝓤 (UniformSpace.Completion α) = ⨅ ε, 𝓟 {p | dist p.1 p.2 < ↑ε}
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>𝓤 (UniformSpace.Completion α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : UniformSpace.Completion α<VAR>h : dist x y = 0<GOAL>x = y
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>Isometry ↑α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>edist (↑α x) (↑α y) = edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>MetricSpace β<VAR>CompleteSpace β<VAR>f : α → β<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<GOAL>LipschitzWith K (UniformSpace.Completion.extension f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<GOAL>LipschitzWith K (UniformSpace.Completion.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>MetricSpace β<VAR>CompleteSpace β<VAR>f : α → β<VAR>h : Isometry f<GOAL>Isometry (UniformSpace.Completion.extension f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<GOAL>Isometry (UniformSpace.Completion.map f)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>f : Filter α<GOAL>Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<GOAL>Cauchy f ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<GOAL>Cauchy f ↔ f.NeBot ∧ ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>l : Filter α<VAR>hl : l.NeBot<GOAL>Cauchy l ↔ l ×ˢ l ≤ 𝓤 α
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>l : Filter α<VAR>h : Cauchy l<GOAL>Cauchy ↑(Ultrafilter.of l)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter β<VAR>f : β → α<GOAL>Cauchy (Filter.map f l) ↔ l.NeBot ∧ Filter.Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter β<VAR>hl : l.NeBot<VAR>f : β → α<GOAL>Cauchy (Filter.map f l) ↔ Filter.Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (𝓤 α)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f g : Filter α<VAR>hg : g.NeBot<VAR>h_c : Cauchy f<VAR>h_le : g ≤ f<GOAL>Cauchy g
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f g : Filter α<VAR>h_c : Cauchy f<GOAL>g.NeBot → g ≤ f → Cauchy g
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>a : α<GOAL>Cauchy (𝓝 a)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>a : α<GOAL>Cauchy (pure a)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>l : Filter β<VAR>l.NeBot<VAR>f : β → α<VAR>a : α<VAR>h : Filter.Tendsto f l (𝓝 a)<GOAL>Cauchy (Filter.map f l)
<VAR>β : Type v<VAR>u v : UniformSpace β<VAR>F : Filter β<VAR>huv : u ≤ v<VAR>hF : Cauchy F<GOAL>Cauchy F
<VAR>β : Type v<VAR>u v : UniformSpace β<VAR>F : Filter β<GOAL>Cauchy F ↔ Cauchy F ∧ Cauchy F
<VAR>β : Type v<VAR>ι : Sort u_1<VAR>Nonempty ι<VAR>u : ι → UniformSpace β<VAR>l : Filter β<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy l
<VAR>β : Type v<VAR>ι : Sort u_1<VAR>u : ι → UniformSpace β<VAR>l : Filter β<VAR>l.NeBot<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy l
<VAR>α : Type u<VAR>β : Type v<VAR>u : UniformSpace β<VAR>f : α → β<VAR>l : Filter α<GOAL>Cauchy l ↔ Cauchy (Filter.map f l)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>F : Filter (α × β)<GOAL>Cauchy F ↔ Cauchy (Filter.map Prod.fst F) ∧ Cauchy (Filter.map Prod.snd F)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>f : Filter α<VAR>g : Filter β<VAR>hf : Cauchy f<VAR>hg : Cauchy g<GOAL>Cauchy (f ×ˢ g)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t<GOAL>f ≤ 𝓝 x
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>hf : Cauchy f<VAR>adhs : ClusterPt x f<GOAL>f ≤ 𝓝 x
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>x : α<VAR>hf : Cauchy f<GOAL>f ≤ 𝓝 x ↔ ClusterPt x f
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>f : Filter α<VAR>m : α → β<VAR>hf : Cauchy f<VAR>hm : UniformContinuous m<GOAL>Cauchy (Filter.map m f)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : Cauchy f<VAR>hm : Filter.comap (fun p => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α<VAR>(Filter.comap m f).NeBot<GOAL>Cauchy (Filter.comap m f)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>f : Filter β<VAR>m : α → β<VAR>hf : Cauchy f<VAR>hm : Filter.comap (fun p => (m p.1, m p.2)) (𝓤 β) ≤ 𝓤 α<GOAL>(Filter.comap m f).NeBot → Cauchy (Filter.comap m f)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Preorder β<VAR>u : β → α<VAR>h : CauchySeq u<GOAL>Filter.Tendsto (Prod.map u u) Filter.atTop (𝓤 α)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Preorder β<VAR>u : β → α<VAR>hu : CauchySeq u<GOAL>Nonempty β
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>β : Type u_1<VAR>SemilatticeSup β<VAR>u : β → α<VAR>h : CauchySeq u<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<GOAL>∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>SemilatticeSup β<VAR>Nonempty β<VAR>f : β → α<VAR>x : α<VAR>hx : Filter.Tendsto f Filter.atTop (𝓝 x)<GOAL>CauchySeq f
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>SemilatticeSup β<VAR>Nonempty β<VAR>x : α<GOAL>CauchySeq fun x_1 => x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (𝓤 α)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Type u_1<VAR>Preorder β<VAR>SemilatticeSup γ<VAR>Nonempty γ<VAR>f : β → α<VAR>hf : CauchySeq f<VAR>g : γ → β<VAR>hg : Filter.Tendsto g Filter.atTop Filter.atTop<GOAL>CauchySeq (f ∘ g)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>SemilatticeSup β<VAR>NoMaxOrder β<VAR>Nonempty β<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>f : β → ℕ<VAR>hf : Function.Injective f<GOAL>CauchySeq (u ∘ f)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : ℕ → ℕ<VAR>hf : Function.Bijective f<VAR>u : ℕ → α<GOAL>CauchySeq (u ∘ f) ↔ CauchySeq u
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>f g : ℕ → ℕ<VAR>hf : Filter.Tendsto f Filter.atTop Filter.atTop<VAR>hg : Filter.Tendsto g Filter.atTop Filter.atTop<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>u : ℕ → α<GOAL>CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>u : ℕ → α<GOAL>CauchySeq u ↔ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>UniformSpace β<VAR>Preorder γ<VAR>Preorder δ<VAR>u : γ → α<VAR>v : δ → β<VAR>hu : CauchySeq u<VAR>hv : CauchySeq v<GOAL>CauchySeq (Prod.map u v)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Type u_1<VAR>UniformSpace β<VAR>Preorder γ<VAR>u : γ → α<VAR>v : γ → β<VAR>hu : CauchySeq u<VAR>hv : CauchySeq v<GOAL>CauchySeq fun x => (u x, v x)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>SemilatticeSup β<VAR>u : β → α<VAR>hu : CauchySeq u<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<GOAL>∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) ∈ V
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Type u_1<VAR>UniformSpace β<VAR>Preorder γ<VAR>f : α → β<VAR>hf : UniformContinuous f<VAR>u : γ → α<VAR>hu : CauchySeq u<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>a : α<VAR>hu : Filter.Tendsto u Filter.atTop (𝓝 a)<GOAL>∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Preorder β<VAR>u : β → α<VAR>hu : CauchySeq u<VAR>ι : Type u_1<VAR>f : ι → β<VAR>p : Filter ι<VAR>p.NeBot<VAR>hf : Filter.Tendsto f p Filter.atTop<VAR>a : α<VAR>ha : Filter.Tendsto (u ∘ f) p (𝓝 a)<GOAL>Filter.Tendsto u Filter.atTop (𝓝 a)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>u : ℕ → α<VAR>k : ℕ<GOAL>(CauchySeq fun n => u (n + k)) ↔ CauchySeq u
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<GOAL>CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>γ : Sort u_1<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<VAR>p : γ → Prop<VAR>s : γ → Set (α × α)<VAR>H : (𝓤 α).HasBasis p s<GOAL>CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>SemilatticeSup β<VAR>Nonempty β<VAR>U : β → Set (α × α)<VAR>hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>f : β → α<VAR>hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N<GOAL>CauchySeq f
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>IsComplete s ↔ ∀ (l : Filter α), Cauchy l → l ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x l
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ 𝓟 s → ∃ x ∈ s, ↑l ≤ 𝓝 x
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<VAR>hs : IsComplete s<VAR>ht : IsComplete t<GOAL>IsComplete (s ∪ t)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>s : ι → Set α<VAR>hs : ∀ (i : ι), IsComplete (s i)<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<VAR>hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j<GOAL>IsComplete (⋃ i, s i)
<VAR>α : Type u<VAR>UniformSpace α<VAR>self : CompleteSpace α<VAR>f : Filter α<GOAL>Cauchy f → ∃ x, f ≤ 𝓝 x
<VAR>α : Type u<VAR>UniformSpace α<VAR>CompleteSpace α<GOAL>IsComplete Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>CompleteSpace (α × β)<VAR>h : Nonempty β<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>CompleteSpace (α × β)<VAR>h : Nonempty α<GOAL>CompleteSpace β
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>Nonempty α<VAR>Nonempty β<GOAL>CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>h : IsComplete Set.univ<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<GOAL>CompleteSpace α ↔ IsComplete Set.univ
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<GOAL>CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ 𝓝 x
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>CompleteSpace α<VAR>l : Filter α<VAR>l.NeBot<GOAL>Cauchy l ↔ ∃ x, l ≤ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>CompleteSpace α<VAR>l : Filter β<VAR>f : β → α<VAR>l.NeBot<GOAL>Cauchy (Filter.map f l) ↔ ∃ x, Filter.Tendsto f l (𝓝 x)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Preorder β<VAR>CompleteSpace α<VAR>u : β → α<VAR>H : CauchySeq u<GOAL>∃ x, Filter.Tendsto u Filter.atTop (𝓝 x)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Preorder β<VAR>K : Set α<VAR>h₁ : IsComplete K<VAR>u : β → α<VAR>h₂ : ∀ (n : β), u n ∈ K<VAR>h₃ : CauchySeq u<GOAL>∃ v ∈ K, Filter.Tendsto u Filter.atTop (𝓝 v)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>CompleteSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<GOAL>f ≤ 𝓝 (lim f)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>Preorder β<VAR>CompleteSpace α<VAR>u : β → α<VAR>h : CauchySeq u<GOAL>Filter.Tendsto u Filter.atTop (𝓝 (limUnder Filter.atTop u))
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>CompleteSpace α<VAR>s : Set α<VAR>h : IsClosed s<GOAL>IsComplete s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>U : ι → Set (α × α)<VAR>H : (𝓤 α).HasBasis p U<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>h : ∀ V ∈ 𝓤 α, SymmetricRel V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, UniformSpace.ball y V<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s₁ s₂ : Set α<VAR>hs : s₁ ⊆ s₂<VAR>h : TotallyBounded s₂<GOAL>TotallyBounded s₁
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>h : TotallyBounded s<GOAL>TotallyBounded (closure s)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>TotallyBounded (closure s) ↔ TotallyBounded s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>Finite ι<VAR>s : ι → Set α<GOAL>TotallyBounded (⋃ i, s i) ↔ ∀ (i : ι), TotallyBounded (s i)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>ι : Type u_1<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set α<GOAL>TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>S : Set (Set α)<VAR>hS : S.Finite<GOAL>TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>a : α<GOAL>TotallyBounded {a}
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<GOAL>TotallyBounded ∅
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<GOAL>TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<VAR>hs : TotallyBounded s<VAR>ht : TotallyBounded t<GOAL>TotallyBounded (s ∪ t)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>a : α<VAR>s : Set α<GOAL>TotallyBounded (insert a s) ↔ TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>hf : UniformContinuous f<GOAL>TotallyBounded (f '' s)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>f : Ultrafilter α<VAR>hs : TotallyBounded s<VAR>h : ↑f ≤ 𝓟 s<GOAL>Cauchy ↑f
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ 𝓟 s → Cauchy ↑f
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<GOAL>IsCompact s ↔ TotallyBounded s ∧ IsComplete s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>h : IsCompact s<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : Set α<VAR>h : IsCompact s<GOAL>IsComplete s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>CompleteSpace α<VAR>s : Set α<VAR>ht : TotallyBounded s<VAR>hc : IsClosed s<GOAL>IsCompact s
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>s : ℕ → α<VAR>hs : CauchySeq s<GOAL>TotallyBounded (Set.range s)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>n : ℕ<GOAL>SequentiallyComplete.setSeq hf U_mem n ∈ f
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>SequentiallyComplete.setSeq hf U_mem n ⊆ SequentiallyComplete.setSeq hf U_mem m
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>n : ℕ<GOAL>SequentiallyComplete.setSeq hf U_mem n ⊆ ↑(SequentiallyComplete.setSeqAux hf U_mem n)
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>N m n : ℕ<VAR>hm : N ≤ m<VAR>hn : N ≤ n<GOAL>SequentiallyComplete.setSeq hf U_mem m ×ˢ SequentiallyComplete.setSeq hf U_mem n ⊆ U N
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>n : ℕ<GOAL>SequentiallyComplete.seq hf U_mem n ∈ SequentiallyComplete.setSeq hf U_mem n
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>N m n : ℕ<VAR>hm : N ≤ m<VAR>hn : N ≤ n<GOAL>(SequentiallyComplete.seq hf U_mem m, SequentiallyComplete.seq hf U_mem n) ∈ U N
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<GOAL>CauchySeq (SequentiallyComplete.seq hf U_mem)