ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>δ ε : ℝ<VAR>h : δ + ε < dist x y<GOAL>Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Disjoint (Metric.sphere x ε) (Metric.ball x ε)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.ball x ε ∪ Metric.sphere x ε = Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.sphere x ε ∪ Metric.ball x ε = Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>x ∈ Metric.ball y ε ↔ y ∈ Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>x ∈ Metric.closedBall y ε ↔ y ∈ Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>x ∈ Metric.sphere y ε ↔ y ∈ Metric.sphere x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε₁ ε₂ : ℝ<VAR>h : ε₁ ≤ ε₂<GOAL>Metric.ball x ε₁ ⊆ Metric.ball x ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.closedBall x ε = ⋂ δ, ⋂ (_ : δ > ε), Metric.ball x δ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : ε₁ + dist x y ≤ ε₂<GOAL>Metric.ball x ε₁ ⊆ Metric.ball y ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε₁ ε₂ : ℝ<VAR>h : ε₁ ≤ ε₂<GOAL>Metric.closedBall x ε₁ ⊆ Metric.closedBall x ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : ε₁ + dist x y ≤ ε₂<GOAL>Metric.closedBall x ε₁ ⊆ Metric.closedBall y ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε₁ ε₂ : ℝ<VAR>h : ε₁ < ε₂<GOAL>Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : ε₁ + dist x y < ε₂<GOAL>Metric.closedBall x ε₁ ⊆ Metric.ball y ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : (Metric.closedBall x ε₁ ∩ Metric.closedBall y ε₂).Nonempty<GOAL>dist x y ≤ ε₁ + ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : (Metric.closedBall x ε₁ ∩ Metric.ball y ε₂).Nonempty<GOAL>dist x y < ε₁ + ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : (Metric.ball x ε₁ ∩ Metric.closedBall y ε₂).Nonempty<GOAL>dist x y < ε₁ + ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : (Metric.ball x ε₁ ∩ Metric.ball y ε₂).Nonempty<GOAL>dist x y < ε₁ + ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>⋃ n, Metric.closedBall x ↑n = Set.univ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>⋃ n, s ∩ Metric.closedBall x ↑n = s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε₁ ε₂ : ℝ<VAR>h : dist x y ≤ ε₂ - ε₁<GOAL>Metric.ball x ε₁ ⊆ Metric.ball y ε₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>y : α<VAR>h : y ∈ Metric.ball x (ε / 2)<GOAL>Metric.ball y (ε / 2) ⊆ Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<VAR>h : y ∈ Metric.ball x ε<GOAL>∃ ε' > 0, Metric.ball y ε' ⊆ Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>p : α → Prop<VAR>x : α<VAR>H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.closedBall x R, p y<VAR>y : α<GOAL>p y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>p : α → Prop<VAR>x : α<VAR>H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.ball x R, p y<VAR>y : α<GOAL>p y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in Filter.atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>c : ℝ<GOAL>Bornology.IsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>PseudoMetricSpace.toUniformSpace = UniformSpace.ofDist dist ⋯ ⋯ ⋯
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>(𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | dist p.1 p.2 < ε}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>β : Type u_3<VAR>p : β → Prop<VAR>f : β → ℝ<VAR>hf₀ : ∀ (i : β), p i → 0 < f i<VAR>hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε<GOAL>(𝓤 α).HasBasis p fun i => {p | dist p.1 p.2 < f i}
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>(𝓤 α).HasBasis (fun r => 0 < r) fun r => {p | dist p.1 p.2 < ↑r}
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>(𝓤 α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 < 1 / (↑n + 1)}
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>(𝓤 α).HasBasis (fun n => 0 < n) fun n => {p | dist p.1 p.2 < 1 / ↑n}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>r : ℝ<VAR>h0 : 0 < r<VAR>h1 : r < 1<GOAL>(𝓤 α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 < r ^ n}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>R : ℝ<VAR>hR : 0 < R<GOAL>(𝓤 α).HasBasis (fun r => 0 < r ∧ r < R) fun r => {p | dist p.1 p.2 < r}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>β : Type u_3<VAR>p : β → Prop<VAR>f : β → ℝ<VAR>hf₀ : ∀ (x : β), p x → 0 < f x<VAR>hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε<GOAL>(𝓤 α).HasBasis p fun x => {p | dist p.1 p.2 ≤ f x}
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>(𝓤 α).HasBasis (fun x => 0 < x) fun ε => {p | dist p.1 p.2 ≤ ε}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>r : ℝ<VAR>h0 : 0 < r<VAR>h1 : r < 1<GOAL>(𝓤 α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 ≤ r ^ n}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set (α × α)<GOAL>s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, dist a b < ε → (a, b) ∈ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>{p | dist p.1 p.2 < ε} ∈ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<GOAL>UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist (f x) (f y) ≤ ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<GOAL>UniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>h : UniformEmbedding f<GOAL>(∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>TotallyBounded s ↔ ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.ball y ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε<GOAL>TotallyBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>ε : ℝ<GOAL>ε > 0 → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, Metric.ball y ε
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>p' : Filter β<GOAL>TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<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, dist (f y) (F n y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<VAR>s : Set β<GOAL>TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>F : ι → β → α<VAR>f : β → α<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : Filter α<GOAL>Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun x => 0 < x) (Metric.ball x)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>p : α → Prop<GOAL>(∀ᶠ (y : α) in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>p : α → Prop<GOAL>(∀ᶠ (y : α) in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ y ∈ Metric.ball x ε, p y
<VAR>α : Type u<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : α × ι → Prop<GOAL>(∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
<VAR>α : Type u<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>f : Filter ι<VAR>x₀ : α<VAR>p : ι × α → Prop<GOAL>(∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun ε => 0 < ε) (Metric.closedBall x)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun x => True) fun n => Metric.ball x (1 / (↑n + 1))
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun n => 0 < n) fun n => Metric.ball x (1 / ↑n)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<VAR>h0 : 0 < r<VAR>h1 : r < 1<GOAL>(𝓝 x).HasBasis (fun x => True) fun n => Metric.ball x (r ^ n)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<VAR>h0 : 0 < r<VAR>h1 : r < 1<GOAL>(𝓝 x).HasBasis (fun x => True) fun n => Metric.closedBall x (r ^ n)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>IsOpen (Metric.ball x ε)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>Metric.ball x ε ∈ 𝓝 x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>ε0 : 0 < ε<GOAL>Metric.closedBall x ε ∈ 𝓝 x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x c : α<VAR>ε : ℝ<VAR>h : x ∈ Metric.ball c ε<GOAL>Metric.closedBall c ε ∈ 𝓝 x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>(𝓝[s] x).HasBasis (fun ε => 0 < ε) fun ε => Metric.ball x ε ∩ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<GOAL>s ∈ 𝓝[t] x ↔ ∃ ε > 0, Metric.ball x ε ∩ t ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>PseudoMetricSpace β<VAR>t : Set β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Filter.Tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Filter.Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>b : β<GOAL>Filter.Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, dist x a < δ → dist (f x) b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<GOAL>ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, dist x a < δ → dist (f x) (f a) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<GOAL>ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<GOAL>Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), dist a b < δ → dist (f a) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : Filter β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<GOAL>ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s : Set β<GOAL>ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f : β → α<VAR>s : Set β<GOAL>ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 a, dist (f x) (f a) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u Filter.atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>NoMaxOrder β<VAR>u : β → α<VAR>a : α<GOAL>Filter.Tendsto u Filter.atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε
<VAR>α : Type u_3<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>IsOpen {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>DiscreteTopology ↑s<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ ε > 0, Metric.ball x ε ∩ s = {x}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>DiscreteTopology ↑s<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ ε > 0, Metric.closedBall x ε ∩ s = {x}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : Dense s<VAR>x : α<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ y ∈ s, dist x y < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>β : Type u_3<VAR>f : β → α<VAR>hf : DenseRange f<VAR>x : α<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ y, dist x (f y) < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x x_1 => r ≤ dist x x_1
<VAR>α : Type u_3<VAR>PseudoMetricSpace α<VAR>r : ℝ<VAR>hpos : 0 < r<VAR>hr : Pairwise fun x x_1 => r ≤ dist x x_1<GOAL>DiscreteTopology α
<VAR>α : Type u_3<VAR>d : α → α → ℝ≥0<GOAL>⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε} = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>EMetric.ball x ⊤ = Set.univ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>EMetric.ball x (ENNReal.ofReal ε) = Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0<GOAL>EMetric.ball x ↑ε = Metric.ball x ↑ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>h : 0 ≤ ε<GOAL>EMetric.closedBall x (ENNReal.ofReal ε) = Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ≥0<GOAL>EMetric.closedBall x ↑ε = Metric.closedBall x ↑ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>Inseparable x y ↔ dist x y = 0
<VAR>α : Type u_3<VAR>U : UniformSpace α<VAR>m : PseudoMetricSpace α<VAR>H : 𝓤 α = 𝓤 α<GOAL>m.replaceUniformity H = m
<VAR>γ : Type u_3<VAR>U : TopologicalSpace γ<VAR>m : PseudoMetricSpace γ<VAR>H : U = UniformSpace.toTopologicalSpace<GOAL>m.replaceTopology H = m
<VAR>α : Type u_3<VAR>m : PseudoMetricSpace α<VAR>B : Bornology α<VAR>H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s<GOAL>m.replaceBornology H = m
<VAR>x y : ℝ<GOAL>dist x y = |x - y|
<VAR>x y : ℝ<GOAL>nndist x y = Real.nnabs (x - y)
<VAR>x y : ℝ<GOAL>nndist x y = Real.nnabs (y - x)
<VAR>x : ℝ<GOAL>dist x 0 = |x|
<VAR>x y : ℝ<GOAL>x - y ≤ dist x y
<VAR>x r : ℝ<GOAL>Metric.ball x r = Set.Ioo (x - r) (x + r)
<VAR>x r : ℝ<GOAL>Metric.closedBall x r = Set.Icc (x - r) (x + r)
<VAR>x y : ℝ<GOAL>Set.Ioo x y = Metric.ball ((x + y) / 2) ((y - x) / 2)
<VAR>x y : ℝ<GOAL>Set.Icc x y = Metric.closedBall ((x + y) / 2) ((y - x) / 2)
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>𝓤 α = Filter.comap (fun p => dist p.1 p.2) (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ Filter.Tendsto (fun n => dist (u n.1) (u n.2)) Filter.atTop (𝓝 0)
<VAR>α : Type u<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>f : ι → α × α<VAR>p : Filter ι<GOAL>Filter.Tendsto f p (𝓤 α) ↔ Filter.Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0)
<VAR>α : Type u<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>f₁ f₂ : ι → α<VAR>p : Filter ι<VAR>a : α<VAR>h₁ : Filter.Tendsto f₁ p (𝓝 a)<VAR>h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)<GOAL>Filter.Tendsto f₂ p (𝓝 a)
<VAR>α : Type u<VAR>ι : Type u_2<VAR>PseudoMetricSpace α<VAR>f₁ f₂ : ι → α<VAR>p : Filter ι<VAR>a : α<VAR>h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)<GOAL>Filter.Tendsto f₁ p (𝓝 a) ↔ Filter.Tendsto f₂ p (𝓝 a)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>dist (dist x z) (dist y z) ≤ dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>dist (dist x y) (dist x z) ≤ dist y z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y x' y' : α<GOAL>dist (dist x y) (dist x' y') ≤ dist x x' + dist y y'
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>a : α<GOAL>Filter.comap (fun x => dist x a) (𝓝 0) = 𝓝 a
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>x : Filter β<VAR>a : α<GOAL>Filter.Tendsto f x (𝓝 a) ↔ Filter.Tendsto (fun b => dist (f b) a) x (𝓝 0)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.ball x ε ⊆ interior (Metric.closedBall x ε)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>e : β → α<VAR>a : α<GOAL>a ∈ closure (Set.range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>e : β → α<VAR>a : α<GOAL>a ∈ closure (Set.range e) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>a : α<GOAL>a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.ball x r ∩ s).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<GOAL>DenseRange f ↔ ∀ (x : α), ∀ r > 0, ∃ y, dist x (f y) < r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>TopologicalSpace β<VAR>hf : Inducing f<VAR>s : Set α<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>TopologicalSpace.IsSeparable (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>TopologicalSpace β<VAR>hf : Embedding f<VAR>s : Set α<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>TopologicalSpace.IsSeparable (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>TopologicalSpace.IsSeparable (f '' s)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>TopologicalSpace.IsSeparable s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>e : ℝ<VAR>he : 0 < e<GOAL>∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ x ∈ t, Metric.ball x e
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>c : ι → Set α<VAR>hs : IsCompact s<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i, c i<GOAL>∃ δ > 0, ∀ x ∈ s, ∃ i, Metric.ball x δ ⊆ c i
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>c : Set (Set α)<VAR>hs : IsCompact s<VAR>hc₁ : ∀ t ∈ c, IsOpen t<VAR>hc₂ : s ⊆ ⋃₀ c<GOAL>∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, Metric.ball x δ ⊆ t
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.Limits.HasLimits C<VAR>X : TopCat<VAR>F : J ⥤ TopCat.Presheaf C X<VAR>H : ∀ (j : J), (F.obj j).IsSheaf<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>c.pt.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.Limits.HasLimits C<VAR>X : TopCat<VAR>F : J ⥤ TopCat.Presheaf C X<VAR>H : ∀ (j : J), (F.obj j).IsSheaf<GOAL>(CategoryTheory.Limits.limit F).IsSheaf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>G.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.HasLimitsOfSize.{v, v, v₁, u₁} C<VAR>CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v₁, v₂, u₁, u₂} G<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ TopCat.Presheaf.IsSheaf (F ⋙ G)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>G : C ⥤ D<VAR>G.ReflectsIsomorphisms<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits G<VAR>X : TopCat<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ TopCat.Presheaf.IsSheaf (F ⋙ G)
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>VAdd M X<VAR>self : IsometricVAdd M X<VAR>c : M<GOAL>Isometry fun x => c +ᵥ x
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>SMul M X<VAR>self : IsometricSMul M X<VAR>c : M<GOAL>Isometry fun x => c • x
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>VAdd M X<VAR>IsometricVAdd M X<VAR>c : M<GOAL>Isometry fun x => c +ᵥ x
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>SMul M X<VAR>IsometricSMul M X<VAR>c : M<GOAL>Isometry fun x => c • x
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>SMul M X<VAR>IsometricSMul M X<VAR>c : M<VAR>x y : X<GOAL>edist (c • x) (c • y) = edist x y
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>VAdd M X<VAR>IsometricVAdd M X<VAR>c : M<VAR>x y : X<GOAL>edist (c +ᵥ x) (c +ᵥ y) = edist x y
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>VAdd M X<VAR>IsometricVAdd M X<VAR>c : M<VAR>s : Set X<GOAL>EMetric.diam (c +ᵥ s) = EMetric.diam s
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>SMul M X<VAR>IsometricSMul M X<VAR>c : M<VAR>s : Set X<GOAL>EMetric.diam (c • s) = EMetric.diam s
<VAR>M : Type u<VAR>Add M<VAR>PseudoEMetricSpace M<VAR>IsometricVAdd M M<VAR>a : M<GOAL>Isometry fun x => a + x
<VAR>M : Type u<VAR>Mul M<VAR>PseudoEMetricSpace M<VAR>IsometricSMul M M<VAR>a : M<GOAL>Isometry fun x => a * x
<VAR>M : Type u<VAR>Mul M<VAR>PseudoEMetricSpace M<VAR>IsometricSMul M M<VAR>a b c : M<GOAL>edist (a * b) (a * c) = edist b c
<VAR>M : Type u<VAR>Add M<VAR>PseudoEMetricSpace M<VAR>IsometricVAdd M M<VAR>a b c : M<GOAL>edist (a + b) (a + c) = edist b c
<VAR>M : Type u<VAR>Mul M<VAR>PseudoEMetricSpace M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a : M<GOAL>Isometry fun x => x * a
<VAR>M : Type u<VAR>Add M<VAR>PseudoEMetricSpace M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a : M<GOAL>Isometry fun x => x + a
<VAR>M : Type u<VAR>Add M<VAR>PseudoEMetricSpace M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a b c : M<GOAL>edist (a + c) (b + c) = edist a b
<VAR>M : Type u<VAR>Mul M<VAR>PseudoEMetricSpace M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>edist (a * c) (b * c) = edist a b