ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>(LightProfinite.pullback.isLimit f g).lift s = LightProfinite.pullback.lift f g s.fst s.snd ⋯
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>LightProfinite.pullback.fst f g = CategoryTheory.CategoryStruct.comp (LightProfinite.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.fst f g)
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>LightProfinite.pullback.snd f g = CategoryTheory.CategoryStruct.comp (LightProfinite.pullbackIsoPullback f g).hom (CategoryTheory.Limits.pullback.snd f g)
<VAR>α : Type w<VAR>Finite α<VAR>X : α → LightProfinite<VAR>B : LightProfinite<VAR>e : (a : α) → X a ⟶ B<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (LightProfinite.finiteCoproduct.ι X a) (LightProfinite.finiteCoproduct.desc X e) = e a
<VAR>α : Type w<VAR>Finite α<VAR>X : α → LightProfinite<VAR>B : LightProfinite<VAR>f g : LightProfinite.finiteCoproduct X ⟶ B<VAR>h : ∀ (a : α), CategoryTheory.CategoryStruct.comp (LightProfinite.finiteCoproduct.ι X a) f = CategoryTheory.CategoryStruct.comp (LightProfinite.finiteCoproduct.ι X a) g<GOAL>f = g
<VAR>α : Type w<VAR>Finite α<VAR>X : α → LightProfinite<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X a) (LightProfinite.coproductIsoCoproduct X).inv = LightProfinite.finiteCoproduct.ι X a
<VAR>α : Type w<VAR>Finite α<VAR>X : α → LightProfinite<VAR>a : α<GOAL>Function.Injective ⇑(LightProfinite.finiteCoproduct.ι X a)
<VAR>α : Type w<VAR>Finite α<VAR>X : α → LightProfinite<VAR>R : ↑(LightProfinite.finiteCoproduct X).toTop<GOAL>∃ a r, R = (LightProfinite.finiteCoproduct.ι X a) r
<VAR>α : Type w<VAR>Finite α<VAR>X : α → LightProfinite<VAR>B : LightProfinite<VAR>π : (a : α) → X a ⟶ B<VAR>a : α<VAR>x : (CategoryTheory.forget LightProfinite).obj (X a)<GOAL>(LightProfinite.finiteCoproduct.desc X π) ((LightProfinite.finiteCoproduct.ι X a) x) = (π a) x
<VAR>α : Type u_1<VAR>EMetricSpace α<GOAL>T4Space α
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrder β<VAR>U : Filter (α × α)<VAR>z : β<VAR>D : α → α → β<VAR>H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s<GOAL>U = ⨅ ε, ⨅ (_ : ε > z), 𝓟 {p | D p.1 p.2 < ε}
<VAR>α : Type u<VAR>self : PseudoEMetricSpace α<VAR>x : α<GOAL>edist x x = 0
<VAR>α : Type u<VAR>self : PseudoEMetricSpace α<VAR>x y z : α<GOAL>edist x z ≤ edist x y + edist y z
<VAR>α : Type u<VAR>self : PseudoEMetricSpace α<VAR>x y : α<GOAL>edist x y = edist y x
<VAR>α : Type u<VAR>self : PseudoEMetricSpace α<GOAL>𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
<VAR>α : Type u_2<VAR>m m' : PseudoEMetricSpace α<VAR>h : PseudoEMetricSpace.toEDist = PseudoEMetricSpace.toEDist<GOAL>m = m'
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y z : α<GOAL>edist x y ≤ edist z x + edist z y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y z : α<GOAL>edist x y ≤ edist x z + edist y z
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y z : α<VAR>h : edist x y = 0<GOAL>edist x z = edist y z
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y z : α<VAR>h : edist x y = 0<GOAL>edist z x = edist z y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>w x y z : α<VAR>hl : edist w x = 0<VAR>hr : edist y z = 0<GOAL>edist w y = edist x z
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y z t : α<GOAL>edist x t ≤ edist x y + edist y z + edist z t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1))
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>d : ℕ → ℝ≥0∞<VAR>hd : ∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k<GOAL>edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>d : ℕ → ℝ≥0∞<VAR>hd : ∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k<GOAL>edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist ⋯ ⋯ ⋯
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set (α × α)<GOAL>s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : β → ℝ≥0∞<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε<GOAL>(𝓤 α).HasBasis p fun x => {p | edist p.1 p.2 < f x}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>p : β → Prop<VAR>f : β → ℝ≥0∞<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε<GOAL>(𝓤 α).HasBasis p fun x => {p | edist p.1 p.2 ≤ f x}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 ≤ ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ε' : ℝ≥0∞<VAR>hε' : 0 < ε'<GOAL>(𝓤 α).HasBasis (fun ε => ε ∈ Set.Ioo 0 ε') fun ε => {p | edist p.1 p.2 < ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ε' : ℝ≥0∞<VAR>hε' : 0 < ε'<GOAL>(𝓤 α).HasBasis (fun ε => ε ∈ Set.Ioo 0 ε') fun ε => {p | edist p.1 p.2 ≤ ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ↑ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 ≤ ↑ε}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(𝓤 α).HasBasis (fun x => True) fun n => {p | edist p.1 p.2 < (↑n)⁻¹}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(𝓤 α).HasBasis (fun x => True) fun n => {p | edist p.1 p.2 < 2⁻¹ ^ n}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<GOAL>{p | edist p.1 p.2 < ε} ∈ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<GOAL>UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<GOAL>UniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : UniformEmbedding f<GOAL>(∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : Filter α<GOAL>Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>B : ℕ → ℝ≥0∞<VAR>hB : ∀ (n : ℕ), 0 < B n<VAR>H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (𝓝 x)<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>(∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)) → CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>p : α → Prop<VAR>x y : Subtype p<GOAL>edist x y = edist ↑x ↑y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : αᵃᵒᵖ<GOAL>edist (AddOpposite.unop x) (AddOpposite.unop y) = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : αᵐᵒᵖ<GOAL>edist (MulOpposite.unop x) (MulOpposite.unop y) = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>edist (MulOpposite.op x) (MulOpposite.op y) = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>edist (AddOpposite.op x) (AddOpposite.op y) = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : ULift.{u_2, u} α<GOAL>edist x y = edist x.down y.down
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>edist { down := x } { down := y } = edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>x y : α × β<GOAL>edist x y = max (edist x.1 y.1) (edist x.2 y.2)
<VAR>β : Type v<VAR>π : β → Type u_2<VAR>Fintype β<VAR>(b : β) → EDist (π b)<VAR>f g : (b : β) → π b<GOAL>edist f g = Finset.univ.sup fun b => edist (f b) (g b)
<VAR>β : Type v<VAR>π : β → Type u_2<VAR>Fintype β<VAR>(b : β) → EDist (π b)<VAR>f g : (b : β) → π b<VAR>b : β<GOAL>edist (f b) (g b) ≤ edist f g
<VAR>β : Type v<VAR>π : β → Type u_2<VAR>Fintype β<VAR>(b : β) → EDist (π b)<VAR>f g : (b : β) → π b<VAR>d : ℝ≥0∞<GOAL>edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>Fintype β<VAR>a b : α<GOAL>(edist (fun x => a) fun x => b) ≤ edist a b
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>Fintype β<VAR>Nonempty β<VAR>a b : α<GOAL>(edist (fun x => a) fun x => b) = edist a b
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<GOAL>y ∈ EMetric.ball x ε ↔ edist y x < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<GOAL>y ∈ EMetric.ball x ε ↔ edist x y < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<GOAL>y ∈ EMetric.closedBall x ε ↔ edist y x ≤ ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<GOAL>y ∈ EMetric.closedBall x ε ↔ edist x y ≤ ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>EMetric.closedBall x ⊤ = Set.univ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<GOAL>EMetric.ball x ε ⊆ EMetric.closedBall x ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<VAR>hy : y ∈ EMetric.ball x ε<GOAL>0 < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>h : 0 < ε<GOAL>x ∈ EMetric.ball x ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<GOAL>x ∈ EMetric.closedBall x ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<GOAL>x ∈ EMetric.ball y ε ↔ y ∈ EMetric.ball x ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<GOAL>x ∈ EMetric.closedBall y ε ↔ y ∈ EMetric.closedBall x ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>h : ε₁ ≤ ε₂<GOAL>EMetric.ball x ε₁ ⊆ EMetric.ball x ε₂
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>h : ε₁ ≤ ε₂<GOAL>EMetric.closedBall x ε₁ ⊆ EMetric.closedBall x ε₂
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>h : ε₁ + ε₂ ≤ edist x y<GOAL>Disjoint (EMetric.ball x ε₁) (EMetric.ball y ε₂)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ≥0∞<VAR>h : edist x y + ε₁ ≤ ε₂<VAR>h' : edist x y ≠ ⊤<GOAL>EMetric.ball x ε₁ ⊆ EMetric.ball y ε₂
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>ε : ℝ≥0∞<VAR>h : y ∈ EMetric.ball x ε<GOAL>∃ ε' > 0, EMetric.ball y ε' ⊆ EMetric.ball x ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<GOAL>EMetric.ball x ε = ∅ ↔ ε = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>{r | EMetric.closedBall x r ⊆ s}.OrdConnected
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>{r | EMetric.ball x r ⊆ s}.OrdConnected
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>EMetric.ball x 0 = ∅
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) (EMetric.ball x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>(𝓝[s] x).HasBasis (fun ε => 0 < ε) fun ε => EMetric.ball x ε ∩ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) (EMetric.closedBall x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>(𝓝[s] x).HasBasis (fun ε => 0 < ε) fun ε => EMetric.closedBall x ε ∩ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>𝓝 x = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 (EMetric.ball x ε)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ ∃ ε > 0, EMetric.ball x ε ⊆ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s t : Set α<GOAL>s ∈ 𝓝[t] x ↔ ∃ ε > 0, EMetric.ball x ε ∩ t ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>t : Set β<VAR>a : α<VAR>b : β<GOAL>Filter.Tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Filter.Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Filter.Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, EMetric.ball x ε ⊆ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<GOAL>IsOpen (EMetric.ball x ε)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>IsClosed (EMetric.ball x ⊤)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<GOAL>EMetric.ball x ε ∈ 𝓝 x
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<GOAL>EMetric.closedBall x ε ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ≥0∞<GOAL>EMetric.ball x r ×ˢ EMetric.ball y r = EMetric.ball (x, y) r