ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t t' : Set X<VAR>h : IsMetricSeparated s t<VAR>h' : IsMetricSeparated s t'<GOAL>IsMetricSeparated s (t ∪ t')
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>s t t' : Set X<GOAL>IsMetricSeparated s (t ∪ t') ↔ IsMetricSeparated s t ∧ IsMetricSeparated s t'
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set X<VAR>t : Set X<GOAL>IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : Set X<VAR>t : ι → Set X<GOAL>IsMetricSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, IsMetricSeparated s (t i)
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>ι : Type u_2<VAR>I : Finset ι<VAR>s : ι → Set X<VAR>t : Set X<GOAL>IsMetricSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, IsMetricSeparated (s i) t
<VAR>X : Type u_1<VAR>EMetricSpace X<VAR>ι : Type u_2<VAR>I : Finset ι<VAR>s : Set X<VAR>t : ι → Set X<GOAL>IsMetricSeparated s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, IsMetricSeparated s (t i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<GOAL>HolderOnWith C r f ∅
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>x : X<GOAL>HolderOnWith C r f {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>s : Set X<VAR>hs : s.Subsingleton<VAR>C r : ℝ≥0<VAR>f : X → Y<GOAL>HolderOnWith C r f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<GOAL>HolderOnWith C r f Set.univ ↔ HolderWith C r f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<GOAL>HolderOnWith C 1 f s ↔ LipschitzOnWith C f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C : ℝ≥0<VAR>f : X → Y<GOAL>HolderWith C 1 f ↔ LipschitzWith C f
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<GOAL>HolderWith 1 1 id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>h : HolderWith C r f<VAR>s : Set X<GOAL>HolderOnWith C r f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>h : HolderOnWith C r f s<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>h : HolderOnWith C r f s<VAR>x y : X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>d : ℝ≥0∞<VAR>hd : edist x y ≤ d<GOAL>edist (f x) (f y) ≤ ↑C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>PseudoEMetricSpace Z<VAR>s : Set X<VAR>Cg rg : ℝ≥0<VAR>g : Y → Z<VAR>t : Set Y<VAR>hg : HolderOnWith Cg rg g t<VAR>Cf rf : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderOnWith Cf rf f s<VAR>hst : Set.MapsTo f s t<GOAL>HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>PseudoEMetricSpace Z<VAR>Cg rg : ℝ≥0<VAR>g : Y → Z<VAR>t : Set Y<VAR>hg : HolderOnWith Cg rg g t<VAR>Cf rf : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith Cf rf f<VAR>ht : ∀ (x : X), f x ∈ t<GOAL>HolderWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>hf : HolderOnWith C r f s<VAR>h0 : 0 < r<GOAL>UniformContinuousOn f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>hf : HolderOnWith C r f s<VAR>h0 : 0 < r<GOAL>ContinuousOn f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>ht : t ⊆ s<GOAL>HolderOnWith C r f t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>hf : HolderOnWith C r f s<VAR>d : ℝ≥0∞<VAR>hd : EMetric.diam s ≤ d<GOAL>EMetric.diam (f '' s) ≤ ↑C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>hf : HolderOnWith C r f s<GOAL>EMetric.diam (f '' s) ≤ ↑C * EMetric.diam s ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>ht : t ⊆ s<GOAL>EMetric.diam (f '' t) ≤ ↑C * EMetric.diam t ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>ht : t ⊆ s<VAR>d : ℝ≥0∞<VAR>hd : EMetric.diam t ≤ d<GOAL>EMetric.diam (f '' t) ≤ ↑C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>hf : HolderOnWith C r f s<VAR>d : ℝ≥0∞<VAR>hd : EMetric.diam t ≤ d<GOAL>EMetric.diam (f '' (t ∩ s)) ≤ ↑C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>hf : HolderOnWith C r f s<VAR>t : Set X<GOAL>EMetric.diam (f '' (t ∩ s)) ≤ ↑C * EMetric.diam t ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>h : HolderWith C r f<VAR>x y : X<GOAL>edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>h : HolderWith C r f<VAR>x y : X<VAR>d : ℝ≥0∞<VAR>hd : edist x y ≤ d<GOAL>edist (f x) (f y) ≤ ↑C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>PseudoEMetricSpace Z<VAR>Cg rg : ℝ≥0<VAR>g : Y → Z<VAR>hg : HolderWith Cg rg g<VAR>Cf rf : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith Cf rf f<GOAL>HolderWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>PseudoEMetricSpace Z<VAR>Cg rg : ℝ≥0<VAR>g : Y → Z<VAR>hg : HolderWith Cg rg g<VAR>Cf rf : ℝ≥0<VAR>f : X → Y<VAR>s : Set X<VAR>hf : HolderOnWith Cf rf f s<GOAL>HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>h0 : 0 < r<GOAL>UniformContinuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>h0 : 0 < r<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>s : Set X<GOAL>EMetric.diam (f '' s) ≤ ↑C * EMetric.diam s ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoMetricSpace X<VAR>PseudoMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>x y : X<VAR>d : ℝ≥0<VAR>hd : nndist x y ≤ d<GOAL>nndist (f x) (f y) ≤ C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoMetricSpace X<VAR>PseudoMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>x y : X<GOAL>nndist (f x) (f y) ≤ C * nndist x y ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoMetricSpace X<VAR>PseudoMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>x y : X<VAR>d : ℝ<VAR>hd : dist x y ≤ d<GOAL>dist (f x) (f y) ≤ ↑C * d ^ ↑r
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoMetricSpace X<VAR>PseudoMetricSpace Y<VAR>C r : ℝ≥0<VAR>f : X → Y<VAR>hf : HolderWith C r f<VAR>x y : X<GOAL>dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>Continuous (thickenedIndicatorAux δ E)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<GOAL>thickenedIndicatorAux δ E x ≤ 1
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<GOAL>thickenedIndicatorAux δ E x < ⊤
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<GOAL>thickenedIndicatorAux δ E x = 1
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_mem : x ∈ closure E<GOAL>thickenedIndicatorAux δ E x = 1
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<VAR>x_out : x ∉ Metric.thickening δ E<GOAL>thickenedIndicatorAux δ E x = 0
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<GOAL>thickenedIndicatorAux δ₁ E ≤ thickenedIndicatorAux δ₂ E
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>(E.indicator fun x => 1) ≤ thickenedIndicatorAux δ E
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E₁ E₂ : Set α<VAR>subset : E₁ ⊆ E₂<GOAL>thickenedIndicatorAux δ E₁ ≤ thickenedIndicatorAux δ E₂
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_lim : Filter.Tendsto δseq Filter.atTop (𝓝 0)<VAR>E : Set α<GOAL>Filter.Tendsto (fun n => thickenedIndicatorAux (δseq n) E) Filter.atTop (𝓝 ((closure E).indicator fun x => 1))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<GOAL>(thickenedIndicator δ_pos E) x = (thickenedIndicatorAux δ E x).toNNReal
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>⇑(thickenedIndicator δ_pos E) = ENNReal.toNNReal ∘ thickenedIndicatorAux δ E
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<GOAL>(thickenedIndicator δ_pos E) x ≤ 1
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<VAR>x_mem : x ∈ closure E<GOAL>(thickenedIndicator δ_pos E) x = 1
<VAR>X : Type u_2<VAR>PseudoEMetricSpace X<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>F : Set X<VAR>x : X<VAR>hxF : x ∈ closure F<GOAL>1 ≤ (thickenedIndicator δ_pos F) x
<VAR>X : Type u_2<VAR>PseudoEMetricSpace X<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>F : Set X<VAR>x : X<VAR>hxF : x ∈ F<GOAL>1 ≤ (thickenedIndicator δ_pos F) x
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<VAR>x_in_E : x ∈ E<GOAL>(thickenedIndicator δ_pos E) x = 1
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<VAR>x_out : x ∉ Metric.thickening δ E<GOAL>(thickenedIndicator δ_pos E) x = 0
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>(E.indicator fun x => 1) ≤ ⇑(thickenedIndicator δ_pos E)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>δ₁_pos : 0 < δ₁<VAR>δ₂_pos : 0 < δ₂<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<GOAL>⇑(thickenedIndicator δ₁_pos E) ≤ ⇑(thickenedIndicator δ₂_pos E)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E₁ E₂ : Set α<VAR>subset : E₁ ⊆ E₂<GOAL>⇑(thickenedIndicator δ_pos E₁) ≤ ⇑(thickenedIndicator δ_pos E₂)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>δseq : ℕ → ℝ<VAR>δseq_pos : ∀ (n : ℕ), 0 < δseq n<VAR>δseq_lim : Filter.Tendsto δseq Filter.atTop (𝓝 0)<VAR>E : Set α<GOAL>Filter.Tendsto (fun n => ⇑(thickenedIndicator ⋯ E)) Filter.atTop (𝓝 ((closure E).indicator fun x => 1))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>One β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>∀ᶠ (δ : ℝ) in 𝓝[>] 0, (Metric.thickening δ E).mulIndicator f x = (closure E).mulIndicator f x
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>Zero β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>∀ᶠ (δ : ℝ) in 𝓝[>] 0, (Metric.thickening δ E).indicator f x = (closure E).indicator f x
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>Zero β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, (Metric.cthickening δ E).indicator f x = (closure E).indicator f x
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>One β<VAR>f : α → β<VAR>E : Set α<VAR>x : α<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, (Metric.cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>One β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>Filter.Tendsto (fun δ => (Metric.thickening δ E).mulIndicator f) (𝓝[>] 0) (𝓝 ((closure E).mulIndicator f))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>Filter.Tendsto (fun δ => (Metric.thickening δ E).indicator f) (𝓝[>] 0) (𝓝 ((closure E).indicator f))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>Zero β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>Filter.Tendsto (fun δ => (Metric.cthickening δ E).indicator f) (𝓝 0) (𝓝 ((closure E).indicator f))
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>β : Type u_2<VAR>One β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>E : Set α<GOAL>Filter.Tendsto (fun δ => (Metric.cthickening δ E).mulIndicator f) (𝓝 0) (𝓝 ((closure E).mulIndicator f))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ENNReal<VAR>ε_pos : 0 < ε<VAR>x : α<VAR>xC : x ∈ C<GOAL>let D := closure (EMetric.ball x (ε / 2) ∩ C);
Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>ε : ENNReal<VAR>hnonempty : C.Nonempty<VAR>ε_pos : 0 < ε<GOAL>∃ C₀ C₁, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧ (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>C : Set α<VAR>hC : Perfect C<VAR>hnonempty : C.Nonempty<VAR>CompleteSpace α<GOAL>∃ f, Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>PolishSpace α<VAR>C : Set α<VAR>hC : IsClosed C<VAR>hunc : ¬C.Countable<GOAL>∃ f, Set.range f ⊆ C ∧ Continuous f ∧ Function.Injective f
<VAR>F : Type u_1<VAR>X : outParam (Type u_2)<VAR>Y : outParam (Type u_3)<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>EquivLike F X Y<VAR>self : DilationEquivClass F X Y<VAR>f : F<GOAL>∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (f x) (f y) = ↑r * edist x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>⇑e.toEquiv = ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e e' : X ≃ᵈ Y<VAR>h : ∀ (x : X), e x = e' x<GOAL>e = e'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>e.symm.symm = e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<GOAL>Function.Bijective DilationEquiv.symm
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<VAR>x : Y<GOAL>e (e.symm x) = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<VAR>x : X<GOAL>e.symm (e x) = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>Dilation.ratio e.toDilation = Dilation.ratio e
<VAR>X : Type u_4<VAR>PseudoEMetricSpace X<GOAL>⇑(DilationEquiv.refl X) = id
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<GOAL>(DilationEquiv.refl X).symm = DilationEquiv.refl X
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<GOAL>Dilation.ratio (DilationEquiv.refl X) = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>PseudoEMetricSpace Z<VAR>e₁ : X ≃ᵈ Y<VAR>e₂ : Y ≃ᵈ Z<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>(DilationEquiv.refl X).trans e = e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>e.trans (DilationEquiv.refl Y) = e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>e.symm.trans e = DilationEquiv.refl Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>e.trans e.symm = DilationEquiv.refl X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>Function.Surjective ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>Function.Bijective ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>Function.Injective ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>PseudoEMetricSpace Z<VAR>e : X ≃ᵈ Y<VAR>e' : Y ≃ᵈ Z<GOAL>Dilation.ratio (e.trans e') = Dilation.ratio e * Dilation.ratio e'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>Dilation.ratio e.symm = (Dilation.ratio e)⁻¹
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e e' : X ≃ᵈ X<GOAL>e * e' = e'.trans e
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<GOAL>1 = DilationEquiv.refl X
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<GOAL>e⁻¹ = e.symm
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e e' : X ≃ᵈ X<GOAL>⇑(e * e') = ⇑e ∘ ⇑e'
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<GOAL>⇑1 = id
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<GOAL>⇑e⁻¹ = ⇑e.symm
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<GOAL>Dilation.ratio e⁻¹ = (Dilation.ratio e)⁻¹
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<VAR>n : ℕ<GOAL>Dilation.ratio (e ^ n) = Dilation.ratio e ^ n
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<VAR>n : ℤ<GOAL>Dilation.ratio (e ^ n) = Dilation.ratio e ^ n
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<GOAL>DilationEquiv.toPerm e = e.toEquiv
<VAR>X : Type u_1<VAR>PseudoEMetricSpace X<VAR>e : X ≃ᵈ X<VAR>n : ℕ<GOAL>⇑(e ^ n) = (⇑e)^[n]
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵢ Y<VAR>x : X<GOAL>e.toDilationEquiv x = e x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵢ Y<GOAL>e.toDilationEquiv.symm = e.symm.toDilationEquiv
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵢ Y<GOAL>e.toDilationEquiv.toDilation = Isometry.toDilation ⇑e ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵢ Y<GOAL>Dilation.ratio e.toDilationEquiv = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>⇑e.toHomeomorph = ⇑e
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>PseudoEMetricSpace X<VAR>PseudoEMetricSpace Y<VAR>e : X ≃ᵈ Y<GOAL>e.toHomeomorph.symm = e.symm.toHomeomorph
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>F : Type u_3<VAR>PseudoMetricSpace X<VAR>PseudoMetricSpace Y<VAR>EquivLike F X Y<VAR>DilationEquivClass F X Y<VAR>e : F<GOAL>Filter.map (⇑e) (Bornology.cobounded X) = Bornology.cobounded Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>h : AntilipschitzWith K f<VAR>x y : α<GOAL>edist x y < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>h : AntilipschitzWith K f<VAR>x y : α<GOAL>edist x y ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<GOAL>K⁻¹ * nndist x y ≤ nndist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<GOAL>↑K⁻¹ * dist x y ≤ dist (f x) (f y)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<GOAL>Function.Injective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>x y : α<GOAL>(↑K)⁻¹ * edist x y ≤ edist (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>s : Set β<GOAL>EMetric.diam (f ⁻¹' s) ≤ ↑K * EMetric.diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>s : Set α<GOAL>EMetric.diam s ≤ ↑K * EMetric.diam (f '' s)
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>AntilipschitzWith 1 id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>Kg : ℝ≥0<VAR>g : β → γ<VAR>hg : AntilipschitzWith Kg g<VAR>Kf : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith Kf f<GOAL>AntilipschitzWith (Kf * Kg) (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>s : Set α<GOAL>AntilipschitzWith K (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>s : Set β<VAR>hs : ∀ (x : α), f x ∈ s<GOAL>AntilipschitzWith K (Set.codRestrict f s hs)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>s : Set α<VAR>hf : AntilipschitzWith K (s.restrict f)<VAR>g : β → α<VAR>t : Set β<VAR>g_maps : Set.MapsTo g t s<VAR>g_inv : Set.RightInvOn g f t<GOAL>LipschitzWith K (t.restrict g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>g : β → α<VAR>t : Set β<VAR>h : Set.RightInvOn g f t<GOAL>LipschitzWith K (t.restrict g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>g : β → α<VAR>hg : Function.RightInverse g f<GOAL>LipschitzWith K g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<GOAL>Filter.comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>hfc : UniformContinuous f<GOAL>UniformInducing f
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>hfc : UniformContinuous f<GOAL>UniformEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>CompleteSpace α<VAR>hf : AntilipschitzWith K f<VAR>hfc : UniformContinuous f<GOAL>IsComplete (Set.range f)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>PseudoEMetricSpace α<VAR>EMetricSpace β<VAR>CompleteSpace α<VAR>f : α → β<VAR>K : ℝ≥0<VAR>hf : AntilipschitzWith K f<VAR>hfc : UniformContinuous f<GOAL>IsClosed (Set.range f)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>EMetricSpace α<VAR>EMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>CompleteSpace α<VAR>hf : AntilipschitzWith K f<VAR>hfc : UniformContinuous f<GOAL>ClosedEmbedding f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>AntilipschitzWith 1 Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>Subsingleton α<VAR>K : ℝ≥0<GOAL>AntilipschitzWith K f
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : AntilipschitzWith 0 f<GOAL>Subsingleton α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>s : Set β<VAR>hs : Bornology.IsBounded s<GOAL>Bornology.IsBounded (f ⁻¹' s)