ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ<GOAL>Metric.closedBall x r ×ˢ Metric.closedBall y r = Metric.closedBall (x, y) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x : α × β<VAR>r : ℝ<GOAL>Metric.sphere x r = Metric.sphere x.1 r ×ˢ Metric.closedBall x.2 r ∪ Metric.closedBall x.1 r ×ˢ Metric.sphere x.2 r
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<GOAL>UniformContinuous fun p => dist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun b => dist (f b) (g b)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<GOAL>Continuous fun p => dist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => dist (f b) (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>f g : β → α<VAR>x : Filter β<VAR>a b : α<VAR>hf : Filter.Tendsto f x (𝓝 a)<VAR>hg : Filter.Tendsto g x (𝓝 b)<GOAL>Filter.Tendsto (fun x => dist (f x) (g x)) x (𝓝 (dist a b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f : β → α<GOAL>Continuous f ↔ Continuous fun x => dist (f x.1) (f x.2)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<GOAL>UniformContinuous fun p => nndist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>UniformSpace β<VAR>f g : β → α<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<GOAL>UniformContinuous fun b => nndist (f b) (g b)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<GOAL>Continuous fun p => nndist p.1 p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>f g : β → α<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => nndist (f b) (g b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>f g : β → α<VAR>x : Filter β<VAR>a b : α<VAR>hf : Filter.Tendsto f x (𝓝 a)<VAR>hg : Filter.Tendsto g x (𝓝 b)<GOAL>Filter.Tendsto (fun x => nndist (f x) (g x)) x (𝓝 (nndist a b))
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<GOAL>nndist f g = Finset.univ.sup fun b => nndist (f b) (g b)
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<GOAL>dist f g = ↑(Finset.univ.sup fun b => nndist (f b) (g b))
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<GOAL>nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<VAR>hr : 0 < r<GOAL>nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>Nonempty β<VAR>f g : (b : β) → π b<VAR>r : ℝ<GOAL>dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>Fintype β<VAR>a b : α<GOAL>(dist (fun x => a) fun x => b) ≤ dist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>Fintype β<VAR>a b : α<GOAL>(nndist (fun x => a) fun x => b) ≤ nndist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>Fintype β<VAR>Nonempty β<VAR>a b : α<GOAL>(dist (fun x => a) fun x => b) = dist a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>Fintype β<VAR>Nonempty β<VAR>a b : α<GOAL>(nndist (fun x => a) fun x => b) = nndist a b
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>b : β<GOAL>nndist (f b) (g b) ≤ nndist f g
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>b : β<GOAL>dist (f b) (g b) ≤ dist f g
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>Nonempty β<VAR>x : (b : β) → π b<VAR>r : ℝ<GOAL>Metric.ball x r = Set.univ.pi fun b => Metric.ball (x b) r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>Nonempty β<VAR>x : (b : β) → π b<VAR>r : ℝ<GOAL>Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>h : 0 < r ∨ Nonempty β<GOAL>Metric.sphere x r = (⋃ i, Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_4<VAR>(i : Fin (n + 1)) → PseudoMetricSpace (α i)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>f g : (j : Fin n) → α (i.succAbove j)<GOAL>nndist (i.insertNth x f) (i.insertNth y g) = max (nndist x y) (nndist f g)
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_4<VAR>(i : Fin (n + 1)) → PseudoMetricSpace (α i)<VAR>i : Fin (n + 1)<VAR>x y : α i<VAR>f g : (j : Fin n) → α (i.succAbove j)<GOAL>dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<GOAL>Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<GOAL>Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x y : α<GOAL>edist (f x) (f y) = edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<GOAL>LipschitzWith 1 f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<GOAL>AntilipschitzWith 1 f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>Subsingleton α<GOAL>Isometry f
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>Isometry id
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>δ : Type u_2<VAR>PseudoEMetricSpace δ<VAR>f : α → β<VAR>g : γ → δ<VAR>hf : Isometry f<VAR>hg : Isometry g<GOAL>Isometry (Prod.map f g)
<VAR>ι : Type u_4<VAR>Fintype ι<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>(i : ι) → PseudoEMetricSpace (α i)<VAR>(i : ι) → PseudoEMetricSpace (β i)<VAR>f : (i : ι) → α i → β i<VAR>hf : ∀ (i : ι), Isometry (f i)<GOAL>Isometry fun g i => f i (g i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : Isometry g<VAR>hf : Isometry f<GOAL>Isometry (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>UniformContinuous f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>UniformInducing f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>ι : Type u_2<VAR>f : α → β<VAR>g : ι → α<VAR>a : Filter ι<VAR>b : α<VAR>hf : Isometry f<GOAL>Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto (f ∘ g) a (𝓝 (f b))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>g : β → α<VAR>h : Isometry f<VAR>hg : Function.RightInverse g f<GOAL>Isometry g
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>f ⁻¹' EMetric.ball (f x) r = EMetric.ball x r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>s : Set α<GOAL>EMetric.diam (f '' s) = EMetric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>EMetric.diam (Set.range f) = EMetric.diam Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>Set.MapsTo f (EMetric.ball x r) (EMetric.ball (f x) r)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>Set.MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) r)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>Isometry Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>γ : Type u_2<VAR>TopologicalSpace γ<VAR>hf : Isometry f<VAR>g : γ → α<VAR>s : Set γ<GOAL>ContinuousOn (f ∘ g) s ↔ ContinuousOn g s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>γ : Type u_2<VAR>TopologicalSpace γ<VAR>hf : Isometry f<VAR>g : γ → α<GOAL>Continuous (f ∘ g) ↔ Continuous g
<VAR>α : Type u<VAR>β : Type v<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>UniformEmbedding f
<VAR>α : Type u<VAR>β : Type v<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>Embedding f
<VAR>α : Type u<VAR>γ : Type w<VAR>EMetricSpace α<VAR>CompleteSpace α<VAR>EMetricSpace γ<VAR>f : α → γ<VAR>hf : Isometry f<GOAL>ClosedEmbedding f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>s : Set α<GOAL>Metric.diam (f '' s) = Metric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>Metric.diam (Set.range f) = Metric.diam Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>p : ℝ → Prop<GOAL>f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ<GOAL>f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ<GOAL>f ⁻¹' Metric.ball (f x) r = Metric.ball x r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ<GOAL>f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ<GOAL>Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) r)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ<GOAL>Set.MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<VAR>x : α<VAR>r : ℝ<GOAL>Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>UniformSpace α<VAR>MetricSpace β<VAR>f : α → β<VAR>h : UniformEmbedding f<GOAL>Isometry f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>MetricSpace β<VAR>f : α → β<VAR>h : Embedding f<GOAL>Isometry f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>self : α ≃ᵢ β<GOAL>Isometry self.toFun
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>Function.Injective IsometryEquiv.toEquiv
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>e₁ e₂ : α ≃ᵢ β<GOAL>e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>a : α<GOAL>h a = h.toEquiv a
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>⇑h.toEquiv = ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>e : α ≃ β<VAR>h : Isometry e.toFun<GOAL>⇑{ toEquiv := e, isometry_toFun := h } = ⇑e
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Isometry ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Function.Bijective ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Function.Injective ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Function.Surjective ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x y : α<GOAL>edist (h x) (h y) = edist x y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x y : α<GOAL>dist (h x) (h y) = dist x y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x y : α<GOAL>nndist (h x) (h y) = nndist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Continuous ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>s : Set α<GOAL>EMetric.diam (⇑h '' s) = EMetric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h₁ h₂ : α ≃ᵢ β<VAR>H : ∀ (x : α), h₁ x = h₂ x<GOAL>h₁ = h₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>h₁ : α ≃ᵢ β<VAR>h₂ : β ≃ᵢ γ<VAR>x : α<GOAL>(h₁.trans h₂) x = h₂ (h₁ x)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>h.symm.symm = h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>Function.Bijective IsometryEquiv.symm
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>y : β<GOAL>h (h.symm y) = y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<GOAL>h.symm (h x) = x
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>y : β<GOAL>h.symm y = x ↔ y = h x
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>y : β<GOAL>x = h.symm y ↔ h x = y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>⇑h.symm ∘ ⇑h = id
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>⇑h ∘ ⇑h.symm = id
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Set.range ⇑h = Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Set.image ⇑h.symm = Set.preimage ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Set.preimage ⇑h.symm = Set.image ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>h₁ : α ≃ᵢ β<VAR>h₂ : β ≃ᵢ γ<VAR>x : γ<GOAL>(h₁.trans h₂).symm x = h₁.symm (h₂.symm x)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>EMetric.diam Set.univ = EMetric.diam Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>s : Set β<GOAL>EMetric.diam (⇑h ⁻¹' s) = EMetric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ≥0∞<GOAL>⇑h ⁻¹' EMetric.ball x r = EMetric.ball (h.symm x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ≥0∞<GOAL>⇑h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>⇑h '' EMetric.ball x r = EMetric.ball (h x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>⇑h '' EMetric.closedBall x r = EMetric.closedBall (h x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>h.toHomeomorph.toEquiv = h.toEquiv
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>⇑h.toHomeomorph = ⇑h
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>⇑h.toHomeomorph.symm = ⇑h.symm
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>γ : Type u_2<VAR>TopologicalSpace γ<VAR>h : α ≃ᵢ β<VAR>f : γ → α<VAR>s : Set γ<GOAL>ContinuousOn (⇑h ∘ f) s ↔ ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>γ : Type u_2<VAR>TopologicalSpace γ<VAR>h : α ≃ᵢ β<VAR>f : γ → α<GOAL>Continuous (⇑h ∘ f) ↔ Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>γ : Type u_2<VAR>TopologicalSpace γ<VAR>h : α ≃ᵢ β<VAR>f : β → γ<GOAL>Continuous (f ∘ ⇑h) ↔ Continuous f
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>⇑1 = id
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>e₁ e₂ : α ≃ᵢ α<GOAL>⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>e₁ e₂ : α ≃ᵢ α<VAR>x : α<GOAL>(e₁ * e₂) x = e₁ (e₂ x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>e : α ≃ᵢ α<VAR>x : α<GOAL>e⁻¹ (e x) = x
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>e : α ≃ᵢ α<VAR>x : α<GOAL>e (e⁻¹ x) = x
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>e : α ≃ᵢ β<GOAL>CompleteSpace α ↔ CompleteSpace β
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>CompleteSpace β<VAR>e : α ≃ᵢ β<GOAL>CompleteSpace α
<VAR>ι : Type u_1<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>Unique ι<VAR>Fintype ι<VAR>x : α<VAR>i : ι<GOAL>(IsometryEquiv.funUnique ι α).symm x i = x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>Unique ι<VAR>Fintype ι<VAR>f : (i : ι) → (fun a => α) i<GOAL>(IsometryEquiv.funUnique ι α) f = f default
<VAR>ι : Type u_1<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>Unique ι<VAR>Fintype ι<VAR>x : α<VAR>i : ι<GOAL>(IsometryEquiv.funUnique ι α).invFun x i = x
<VAR>α : Fin 2 → Type u_2<VAR>(i : Fin 2) → PseudoEMetricSpace (α i)<VAR>f : (i : Fin 2) → α i<GOAL>(IsometryEquiv.piFinTwo α) f = (f 0, f 1)
<VAR>α : Fin 2 → Type u_2<VAR>(i : Fin 2) → PseudoEMetricSpace (α i)<VAR>p : α 0 × α 1<VAR>i : Fin (1 + 1)<GOAL>(IsometryEquiv.piFinTwo α).invFun p i = Fin.cons p.1 (Fin.cons p.2 finZeroElim) i
<VAR>α : Fin 2 → Type u_2<VAR>(i : Fin 2) → PseudoEMetricSpace (α i)<VAR>p : α 0 × α 1<VAR>i : Fin (1 + 1)<GOAL>(IsometryEquiv.piFinTwo α).symm p i = Fin.cons p.1 (Fin.cons p.2 finZeroElim) i
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>s : Set α<GOAL>Metric.diam (⇑h '' s) = Metric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>s : Set β<GOAL>Metric.diam (⇑h ⁻¹' s) = Metric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<GOAL>Metric.diam Set.univ = Metric.diam Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ<GOAL>⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ<GOAL>⇑h ⁻¹' Metric.sphere x r = Metric.sphere (h.symm x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : β<VAR>r : ℝ<GOAL>⇑h ⁻¹' Metric.closedBall x r = Metric.closedBall (h.symm x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ<GOAL>⇑h '' Metric.ball x r = Metric.ball (h x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ<GOAL>⇑h '' Metric.sphere x r = Metric.sphere (h x) r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>h : α ≃ᵢ β<VAR>x : α<VAR>r : ℝ<GOAL>⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r
<VAR>α : Type u<VAR>β : Type v<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<GOAL>h.isometryEquivOnRange.toEquiv = Equiv.ofInjective f ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>EMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : Isometry f<VAR>a : α<GOAL>h.isometryEquivOnRange a = ⟨f a, ⋯⟩
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>K : NNReal<VAR>h : Isometry g<GOAL>LipschitzWith K (g ∘ f) ↔ LipschitzWith K f
<VAR>β : Type v<VAR>NormedRing β<VAR>hn : IsAbsoluteValue norm<VAR>f : CauSeq β norm<VAR>CauSeq.IsComplete β norm<GOAL>Filter.Tendsto (↑f) Filter.atTop (𝓝 f.lim)
<VAR>β : Type v<VAR>NormedField β<VAR>f : ℕ → β<VAR>hf : CauchySeq f<GOAL>IsCauSeq norm f
<VAR>β : Type v<VAR>NormedField β<VAR>f : CauSeq β norm<GOAL>CauchySeq ↑f
<VAR>α : Type u<VAR>NormedField α<VAR>u : ℕ → α<GOAL>IsCauSeq norm u ↔ CauchySeq u
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>self : ProperSpace α<VAR>x : α<VAR>r : ℝ<GOAL>IsCompact (Metric.closedBall x r)
<VAR>α : Type u_3<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>x : α<VAR>r : ℝ<GOAL>IsCompact (Metric.sphere x r)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>R : ℝ<VAR>h : ∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)<GOAL>ProperSpace α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>β : Type u_3<VAR>l : Filter β<VAR>l.NeBot<VAR>x : α<VAR>r : β → ℝ<VAR>hr : Filter.Tendsto r l Filter.atTop<VAR>hc : ∀ᶠ (i : β) in l, IsCompact (Metric.closedBall x (r i))<GOAL>ProperSpace α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>B : ℕ → ℝ<VAR>hB : ∀ (n : ℕ), 0 < B n<VAR>H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (𝓝 x)<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>(∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)) → CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>Nonempty β<VAR>SemilatticeSup β<VAR>u : β → α<GOAL>CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε