ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>s : Set α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<GOAL>s.infsep ≤ dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>d : ℝ<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hxy' : dist x y ≤ d<GOAL>s.infsep ≤ d
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>{x, y}.infsep = dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y z : α<VAR>hxy : x ≠ y<VAR>hyz : y ≠ z<VAR>hxz : x ≠ z<GOAL>{x, y, z}.infsep = dist x y ⊓ dist x z ⊓ dist y z
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>hs : s.Nontrivial<VAR>hst : s ⊆ t<GOAL>t.infsep ≤ s.infsep
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>Decidable s.Nontrivial<GOAL>s.infsep = if s.Nontrivial then ⨅ d, Function.uncurry dist ↑d else 0
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s.infsep = ⨅ d, Function.uncurry dist ↑d
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>Decidable s.Nontrivial<VAR>DecidableEq α<VAR>Fintype ↑s<GOAL>s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (Function.uncurry dist) else 0
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>hs : s.Nontrivial<GOAL>s.infsep = s.offDiag.toFinset.inf' ⋯ (Function.uncurry dist)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>Decidable s.Nontrivial<VAR>hsf : s.Finite<GOAL>s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (Function.uncurry dist) else 0
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hsf : s.Finite<VAR>hs : s.Nontrivial<GOAL>s.infsep = ⋯.toFinset.inf' ⋯ (Function.uncurry dist)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (Function.uncurry dist) else 0
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>DecidableEq α<VAR>s : Finset α<VAR>hs : s.offDiag.Nonempty<GOAL>(↑s).infsep = s.offDiag.inf' hs (Function.uncurry dist)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>DecidableEq α<VAR>s : Finset α<VAR>hs : s.offDiag = ∅<GOAL>(↑s).infsep = 0
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>Finite ↑s<VAR>hs : s.Nontrivial<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hsf : s.Finite<VAR>hs : s.Nontrivial<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : Set α<VAR>Finite ↑s<GOAL>s.infsep = 0 ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : Set α<VAR>Finite ↑s<GOAL>0 < s.infsep ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.infsep = 0 ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>0 < s.infsep ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : Finset α<GOAL>(↑s).infsep = 0 ↔ (↑s).Subsingleton
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>s : Finset α<GOAL>0 < (↑s).infsep ↔ (↑s).Nontrivial
<VAR>X : TopCat<VAR>T : ↑X → Type u<GOAL>(X.presheafToTypes T).IsSheaf
<VAR>X : TopCat<VAR>T : Type u<GOAL>(X.presheafToType T).IsSheaf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>self : α →ᵈ β<GOAL>∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (self.toFun x) (self.toFun y) = ↑r * edist x y
<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>self : DilationClass F α β<VAR>f : F<GOAL>∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y<GOAL>⇑{ toFun := f, edist_eq' := h } = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f g : α →ᵈ β<VAR>h : f = g<VAR>x : α<GOAL>f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<VAR>x y : α<VAR>h : x = y<GOAL>f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f g : α →ᵈ β<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f g : α →ᵈ β<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<VAR>h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y<GOAL>{ toFun := ⇑f, edist_eq' := h } = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤<GOAL>Dilation.ratio f = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>Subsingleton α<VAR>DilationClass F α β<VAR>f : F<GOAL>Dilation.ratio f = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>Dilation.ratio f ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>0 < Dilation.ratio f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x y : α<GOAL>edist (f x) (f y) = ↑(Dilation.ratio f) * edist x y
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x y : α<GOAL>nndist (f x) (f y) = Dilation.ratio f * nndist x y
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x y : α<GOAL>dist (f x) (f y) = ↑(Dilation.ratio f) * dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>h₀ : edist x y ≠ 0<VAR>htop : edist x y ≠ ⊤<VAR>hr : edist (f x) (f y) = ↑r * edist x y<GOAL>r = Dilation.ratio f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>F : Type u_8<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>hxy : nndist x y ≠ 0<VAR>hr : nndist (f x) (f y) = r * nndist x y<GOAL>r = Dilation.ratio f
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>F : Type u_6<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>hxy : dist x y ≠ 0<VAR>hr : dist (f x) (f y) = ↑r * dist x y<GOAL>r = Dilation.ratio f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y<GOAL>⇑(Dilation.mkOfNNDistEq f h) = f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α →ᵈ β<VAR>h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y<GOAL>Dilation.mkOfNNDistEq (⇑f) h = f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y<GOAL>⇑(Dilation.mkOfDistEq f h) = f
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α →ᵈ β<VAR>h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y<GOAL>Dilation.mkOfDistEq (⇑f) h = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>∀ (a : α), (Isometry.toDilation f hf) a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : Isometry f<GOAL>Dilation.ratio (Isometry.toDilation f hf) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>LipschitzWith (Dilation.ratio f) ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>AntilipschitzWith (Dilation.ratio f)⁻¹ ⇑f
<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace β<VAR>α : Type u_6<VAR>EMetricSpace α<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>Function.Injective ⇑f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>⇑(Dilation.id α) = id
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>Dilation.ratio (Dilation.id α) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>δ : Type u_6<VAR>PseudoEMetricSpace δ<VAR>f : α →ᵈ β<VAR>g : β →ᵈ γ<VAR>h : γ →ᵈ δ<GOAL>(h.comp g).comp f = h.comp (g.comp f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<GOAL>⇑(g.comp f) = ⇑g ∘ ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<VAR>x : α<GOAL>(g.comp f) x = g (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<VAR>hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤<GOAL>Dilation.ratio (g.comp f) = Dilation.ratio g * Dilation.ratio f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<GOAL>f.comp (Dilation.id α) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α →ᵈ β<GOAL>(Dilation.id β).comp f = f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>1 = Dilation.id α
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f g : α →ᵈ α<GOAL>f * g = f.comp g
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>⇑1 = id
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f g : α →ᵈ α<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<GOAL>Dilation.ratio 1 = 1
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f g : α →ᵈ α<GOAL>Dilation.ratio (f * g) = Dilation.ratio f * Dilation.ratio g
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : α →ᵈ α<GOAL>Dilation.ratioHom f = Dilation.ratio f
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>f : α →ᵈ α<VAR>n : ℕ<GOAL>Dilation.ratio (f ^ n) = Dilation.ratio f ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g₁ g₂ : β →ᵈ γ<VAR>f : α →ᵈ β<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g : β →ᵈ γ<VAR>f₁ f₂ : α →ᵈ β<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>UniformInducing ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>ι : Type u_6<VAR>g : ι → α<VAR>a : Filter ι<VAR>b : α<GOAL>Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto (⇑f ∘ g) a (𝓝 (f b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>Continuous ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>s : Set α<GOAL>EMetric.diam (⇑f '' s) = ↑(Dilation.ratio f) * EMetric.diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>EMetric.diam (Set.range ⇑f) = ↑(Dilation.ratio f) * EMetric.diam Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>Set.MapsTo (⇑f) (EMetric.ball x r) (EMetric.ball (f x) (↑(Dilation.ratio f) * r))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x : α<VAR>r' : ℝ≥0∞<GOAL>Set.MapsTo (⇑f) (EMetric.closedBall x r') (EMetric.closedBall (f x) (↑(Dilation.ratio f) * r'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>γ : Type u_6<VAR>TopologicalSpace γ<VAR>g : γ → α<VAR>s : Set γ<GOAL>ContinuousOn (⇑f ∘ g) s ↔ ContinuousOn g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>γ : Type u_6<VAR>TopologicalSpace γ<VAR>g : γ → α<GOAL>Continuous (⇑f ∘ g) ↔ Continuous g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>EMetricSpace α<VAR>FunLike F α β<VAR>PseudoEMetricSpace β<VAR>DilationClass F α β<VAR>f : F<GOAL>UniformEmbedding ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>EMetricSpace α<VAR>FunLike F α β<VAR>PseudoEMetricSpace β<VAR>DilationClass F α β<VAR>f : F<GOAL>Embedding ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>EMetricSpace α<VAR>FunLike F α β<VAR>CompleteSpace α<VAR>EMetricSpace β<VAR>DilationClass F α β<VAR>f : F<GOAL>ClosedEmbedding ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>MetricSpace α<VAR>Nontrivial α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>g : β →ᵈ γ<VAR>f : α →ᵈ β<GOAL>Dilation.ratio (g.comp f) = Dilation.ratio g * Dilation.ratio f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>s : Set α<GOAL>Metric.diam (⇑f '' s) = ↑(Dilation.ratio f) * Metric.diam s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>Metric.diam (Set.range ⇑f) = ↑(Dilation.ratio f) * Metric.diam Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x : α<VAR>r' : ℝ<GOAL>Set.MapsTo (⇑f) (Metric.ball x r') (Metric.ball (f x) (↑(Dilation.ratio f) * r'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x : α<VAR>r' : ℝ<GOAL>Set.MapsTo (⇑f) (Metric.sphere x r') (Metric.sphere (f x) (↑(Dilation.ratio f) * r'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<VAR>x : α<VAR>r' : ℝ<GOAL>Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(Dilation.ratio f) * r'))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>Filter.Tendsto (⇑f) (Bornology.cobounded α) (Bornology.cobounded β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_4<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>FunLike F α β<VAR>DilationClass F α β<VAR>f : F<GOAL>Filter.comap (⇑f) (Bornology.cobounded β) = Bornology.cobounded α
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(X.presheafToTypes T).obj U = ((x : ↥(Opposite.unop U)) → T ↑x)
<VAR>X : TopCat<VAR>T : ↑X → Type v<VAR>U V : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>f : (X.presheafToTypes T).obj U<GOAL>(X.presheafToTypes T).map i f = fun x => f ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>X : TopCat<VAR>T : Type v<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(X.presheafToType T).obj U = (↥(Opposite.unop U) → T)
<VAR>X : TopCat<VAR>T : Type v<VAR>U V : (TopologicalSpace.Opens ↑X)ᵒᵖ<VAR>i : U ⟶ V<VAR>f : (X.presheafToType T).obj U<GOAL>(X.presheafToType T).map i f = f ∘ fun x => ⟨↑x, ⋯⟩
<VAR>X T : TopCat<VAR>U : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(X.presheafToTop T).obj U = ((TopologicalSpace.Opens.toTopCat X).obj (Opposite.unop U) ⟶ T)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>[x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s, y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ 𝓝 x ≤ 𝓝 y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ⤳ y<GOAL>¬Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ pure x ≤ 𝓝 y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).ker = {y | y ⤳ x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>h : x ⤳ y<VAR>hs : IsOpen s<VAR>hy : y ∈ s<GOAL>x ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hx : x ∉ s<VAR>hy : y ∈ s<GOAL>¬x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>h : x ⤳ y<VAR>hs : IsClosed s<VAR>hx : x ∈ s<GOAL>y ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hx : x ∈ s<VAR>hy : y ∉ s<GOAL>¬x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ y ∈ closure {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ closure {y} ⊆ closure {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>x ⤳ y ↔ ClusterPt y (pure x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>ι : Sort u_7<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 y).HasBasis p s<GOAL>x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>x ⤳ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<GOAL>x ⤳ y → y ⤳ z → x ⤳ z
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>e : x = y<GOAL>x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>h₁ : 𝓝[s] x ≤ 𝓝[s] y<VAR>h₂ : x ∈ s<GOAL>x ⤳ y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>f : X → Y<VAR>h : x ⤳ y<VAR>hy : ContinuousAt f y<GOAL>f x ⤳ f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>f : X → Y<VAR>h : x ⤳ y<VAR>hf : Continuous f<GOAL>f x ⤳ f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>f x ⤳ f y ↔ x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>x y : Subtype p<GOAL>x ⤳ y ↔ ↑x ⤳ ↑y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₁ x₂ : X<VAR>y₁ y₂ : Y<GOAL>(x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₁ x₂ : X<VAR>y₁ y₂ : Y<VAR>hx : x₁ ⤳ x₂<VAR>hy : y₁ ⤳ y₂<GOAL>(x₁, y₁) ⤳ (x₂, y₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a b : X × Y<VAR>h : a ⤳ b<GOAL>a.1 ⤳ b.1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a b : X × Y<VAR>h : a ⤳ b<GOAL>a.2 ⤳ b.2
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>f g : (i : ι) → π i<GOAL>f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>¬x ⤳ y ↔ ∃ S, IsOpen S ∧ y ∈ S ∧ x ∉ S
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f g : X → Y<VAR>DecidablePred fun x => x ∈ s<VAR>hs : IsOpen s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), f x ⤳ g x<GOAL>Continuous (s.piecewise f g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>f g : X → Y<VAR>DecidablePred fun x => x ∈ s<VAR>hs : IsClosed s<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hspec : ∀ (x : X), g x ⤳ f x<GOAL>Continuous (s.piecewise f g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>Monotone f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>closure {x} = Set.Iic x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>StableUnderSpecialization s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>StableUnderGeneralization s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>StableUnderSpecialization sᶜ ↔ StableUnderGeneralization s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>StableUnderGeneralization sᶜ ↔ StableUnderSpecialization s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>StableUnderSpecialization Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>StableUnderSpecialization ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>StableUnderGeneralization Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>StableUnderGeneralization ∅
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>H : ∀ s ∈ S, StableUnderSpecialization s<GOAL>StableUnderSpecialization (⋃₀ S)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>H : ∀ s ∈ S, StableUnderSpecialization s<GOAL>StableUnderSpecialization (⋂₀ S)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>H : ∀ s ∈ S, StableUnderGeneralization s<GOAL>StableUnderGeneralization (⋃₀ S)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>S : Set (Set X)<VAR>H : ∀ s ∈ S, StableUnderGeneralization s<GOAL>StableUnderGeneralization (⋂₀ S)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_7<VAR>S : ι → Set X<VAR>H : ∀ (i : ι), StableUnderSpecialization (S i)<GOAL>StableUnderSpecialization (⋃ i, S i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_7<VAR>S : ι → Set X<VAR>H : ∀ (i : ι), StableUnderSpecialization (S i)<GOAL>StableUnderSpecialization (⋂ i, S i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_7<VAR>S : ι → Set X<VAR>H : ∀ (i : ι), StableUnderGeneralization (S i)<GOAL>StableUnderGeneralization (⋃ i, S i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Sort u_7<VAR>S : ι → Set X<VAR>H : ∀ (i : ι), StableUnderGeneralization (S i)<GOAL>StableUnderGeneralization (⋂ i, S i)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>⋃ x ∈ s, closure {x} = s ↔ StableUnderSpecialization s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>StableUnderSpecialization s ↔ ⋃ x ∈ s, closure {x} = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set Y<VAR>hs : StableUnderSpecialization s<VAR>hf : Continuous f<GOAL>StableUnderSpecialization (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set Y<VAR>hs : StableUnderGeneralization s<VAR>hf : Continuous f<GOAL>StableUnderGeneralization (f ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>SpecializingMap f ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}