ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<GOAL>dimH s = ↑(FiniteDimensional.finrank ℝ E)
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>h : (interior s).Nonempty<GOAL>dimH s = ↑(FiniteDimensional.finrank ℝ E)
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<GOAL>dimH Set.univ = ↑(FiniteDimensional.finrank ℝ E)
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>d : ℝ<VAR>hd : ↑(FiniteDimensional.finrank ℝ E) < d<GOAL>μH[d] = 0
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>s : Set E<VAR>hs : dimH s < ↑(FiniteDimensional.finrank ℝ E)<GOAL>Dense sᶜ
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>s t : Set E<VAR>hf : ContDiffOn ℝ 1 f s<VAR>hc : Convex ℝ s<VAR>ht : t ⊆ s<GOAL>dimH (f '' t) ≤ dimH t
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>h : ContDiff ℝ 1 f<GOAL>dimH (Set.range f) ≤ ↑(FiniteDimensional.finrank ℝ E)
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>f : E → F<VAR>s t : Set E<VAR>h : ContDiffOn ℝ 1 f s<VAR>hc : Convex ℝ s<VAR>ht : t ⊆ s<VAR>htF : dimH t < ↑(FiniteDimensional.finrank ℝ F)<GOAL>Dense (f '' t)ᶜ
<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>FiniteDimensional ℝ F<VAR>f : E → F<VAR>h : ContDiff ℝ 1 f<VAR>hEF : FiniteDimensional.finrank ℝ E < FiniteDimensional.finrank ℝ F<GOAL>Dense (Set.range f)ᶜ
<VAR>X : TopCat<VAR>F : TopCat.Presheaf (CategoryTheory.Discrete Unit) X<GOAL>F.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F G : TopCat.Presheaf C X<VAR>α : F ≅ G<GOAL>F.IsSheaf ↔ G.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F G : TopCat.Presheaf C X<VAR>α : F ≅ G<VAR>h : F.IsSheaf<GOAL>G.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F : TopCat.Sheaf C X<VAR>t : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(𝟙 F).val.app t = 𝟙 (F.val.obj t)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>F G H : TopCat.Sheaf C X<VAR>f : F ⟶ G<VAR>g : G ⟶ H<VAR>t : (TopologicalSpace.Opens ↑X)ᵒᵖ<GOAL>(f ≫ g).val.app t = f.val.app t ≫ g.val.app t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<GOAL>x ∈ Metric.thickening δ s ↔ EMetric.infEdist x s < ENNReal.ofReal δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ Metric.thickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.thickening δ E = (fun x => EMetric.infEdist x E) ⁻¹' Set.Iio (ENNReal.ofReal δ)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>IsOpen (Metric.thickening δ E)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<GOAL>Metric.thickening δ ∅ = ∅
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>hδ : δ ≤ 0<VAR>s : Set α<GOAL>Metric.thickening δ s = ∅
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<GOAL>Metric.thickening δ₁ E ⊆ Metric.thickening δ₂ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E₁ E₂ : Set α<VAR>h : E₁ ⊆ E₂<GOAL>Metric.thickening δ E₁ ⊆ Metric.thickening δ E₂
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<GOAL>x ∈ Metric.thickening δ E ↔ ∃ z ∈ E, edist x z < ENNReal.ofReal δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>δ : ℝ<GOAL>frontier (Metric.thickening δ E) ⊆ {x | EMetric.infEdist x E = ENNReal.ofReal δ}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>A : Set α<GOAL>Pairwise (Disjoint on fun r => frontier (Metric.thickening r A))
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>E ⊆ (Metric.thickening δ (Metric.thickening δ E)ᶜ)ᶜ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.thickening δ (Metric.thickening δ E)ᶜ ⊆ Eᶜ
<VAR>δ : ℝ<VAR>X : Type u<VAR>PseudoMetricSpace X<VAR>E : Set X<VAR>x : X<VAR>h : E.Nonempty<GOAL>x ∈ Metric.thickening δ E ↔ Metric.infDist x E < δ
<VAR>δ : ℝ<VAR>X : Type u<VAR>PseudoMetricSpace X<VAR>E : Set X<VAR>x : X<GOAL>x ∈ Metric.thickening δ E ↔ ∃ z ∈ E, dist x z < δ
<VAR>X : Type u<VAR>PseudoMetricSpace X<VAR>δ : ℝ<VAR>x : X<GOAL>Metric.thickening δ {x} = Metric.ball x δ
<VAR>X : Type u<VAR>PseudoMetricSpace X<VAR>x : X<VAR>E : Set X<VAR>hx : x ∈ E<VAR>δ : ℝ<GOAL>Metric.ball x δ ⊆ Metric.thickening δ E
<VAR>X : Type u<VAR>PseudoMetricSpace X<VAR>δ : ℝ<VAR>E : Set X<GOAL>Metric.thickening δ E = ⋃ x ∈ E, Metric.ball x δ
<VAR>X : Type u<VAR>PseudoMetricSpace X<VAR>δ : ℝ<VAR>E : Set X<VAR>h : Bornology.IsBounded E<GOAL>Bornology.IsBounded (Metric.thickening δ E)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<GOAL>x ∈ Metric.cthickening δ s ↔ EMetric.infEdist x s ≤ ENNReal.ofReal δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>x : α<VAR>h : x ∉ closure E<GOAL>∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : y ∈ E<VAR>h' : edist x y ≤ ENNReal.ofReal δ<GOAL>x ∈ Metric.cthickening δ E
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : y ∈ E<VAR>h' : dist x y ≤ δ<GOAL>x ∈ Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.cthickening δ E = (fun x => EMetric.infEdist x E) ⁻¹' Set.Iic (ENNReal.ofReal δ)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>IsClosed (Metric.cthickening δ E)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<GOAL>Metric.cthickening δ ∅ = ∅
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>hδ : δ ≤ 0<VAR>E : Set α<GOAL>Metric.cthickening δ E = closure E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<GOAL>Metric.cthickening 0 E = closure E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.cthickening (max 0 δ) E = Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<GOAL>Metric.cthickening δ₁ E ⊆ Metric.cthickening δ₂ E
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>δ : ℝ<VAR>hδ : 0 ≤ δ<GOAL>Metric.cthickening δ {x} = Metric.closedBall x δ
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>δ : ℝ<GOAL>Metric.closedBall x δ ⊆ Metric.cthickening δ {x}
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E₁ E₂ : Set α<VAR>h : E₁ ⊆ E₂<GOAL>Metric.cthickening δ E₁ ⊆ Metric.cthickening δ E₂
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ₁ : ℝ≥0<VAR>δ₂ : ℝ<VAR>hlt : ↑δ₁ < δ₂<VAR>E : Set α<GOAL>Metric.cthickening (↑δ₁) E ⊆ Metric.thickening δ₂ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>δ₂_pos : 0 < δ₂<VAR>hlt : δ₁ < δ₂<VAR>E : Set α<GOAL>Metric.cthickening δ₁ E ⊆ Metric.thickening δ₂ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.thickening δ E ⊆ Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<GOAL>Metric.thickening δ₁ E ⊆ Metric.cthickening δ₂ E
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : Bornology.IsBounded E<GOAL>Bornology.IsBounded (Metric.cthickening δ E)
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>r : ℝ<GOAL>IsCompact (Metric.cthickening r s)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.thickening δ E ⊆ interior (Metric.cthickening δ E)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>closure (Metric.thickening δ E) ⊆ Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>closure E ⊆ Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>closure E ⊆ Metric.thickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>E ⊆ Metric.thickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>E ⊆ Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>δ : ℝ<VAR>hδ : 0 < δ<GOAL>Metric.thickening δ E ∈ 𝓝ˢ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>δ : ℝ<VAR>hδ : 0 < δ<GOAL>Metric.cthickening δ E ∈ 𝓝ˢ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s t : Set α<GOAL>Metric.thickening δ (s ∪ t) = Metric.thickening δ s ∪ Metric.thickening δ t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s t : Set α<GOAL>Metric.cthickening δ (s ∪ t) = Metric.cthickening δ s ∪ Metric.cthickening δ t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>f : ι → Set α<GOAL>Metric.thickening δ (⋃ i, f i) = ⋃ i, Metric.thickening δ (f i)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>δ : ℝ<VAR>f : ι → Set α<VAR>I : Set ι<GOAL>Metric.thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, Metric.thickening δ (f i)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>ε : ℝ≥0<GOAL>EMetric.diam (Metric.cthickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>ε : ℝ≥0<GOAL>EMetric.diam (Metric.thickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε
<VAR>ε : ℝ<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hε : 0 ≤ ε<GOAL>Metric.diam (Metric.cthickening ε s) ≤ Metric.diam s + 2 * ε
<VAR>ε : ℝ<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hε : 0 ≤ ε<GOAL>Metric.diam (Metric.thickening ε s) ≤ Metric.diam s + 2 * ε
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<GOAL>Metric.thickening δ (closure s) = Metric.thickening δ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<GOAL>Metric.cthickening δ (closure s) = Metric.cthickening δ s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<GOAL>∃ δ, 0 < δ ∧ Disjoint (Metric.thickening δ s) (Metric.thickening δ t)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : IsCompact s<VAR>ht : IsClosed t<GOAL>∃ δ, 0 < δ ∧ Disjoint (Metric.cthickening δ s) (Metric.cthickening δ t)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hs : IsCompact s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<GOAL>∃ δ, 0 < δ ∧ Metric.cthickening δ s ⊆ t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>LocallyCompactSpace α<VAR>hs : IsCompact s<GOAL>∃ δ, 0 < δ ∧ IsCompact (Metric.cthickening δ s)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hs : IsCompact s<VAR>ht : IsOpen t<VAR>hst : s ⊆ t<GOAL>∃ δ, 0 < δ ∧ Metric.thickening δ s ⊆ t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>(𝓝ˢ K).HasBasis (fun δ => 0 < δ) fun δ => Metric.thickening δ K
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>(𝓝ˢ K).HasBasis (fun δ => 0 < δ) fun δ => Metric.cthickening δ K
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Set.Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Set.Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>Metric.cthickening δ E = ⋂ ε ∈ s, Metric.cthickening ε E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), Metric.cthickening ε E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>s : Set ℝ<VAR>hsδ : s ⊆ Set.Ioi δ<VAR>hs : ∀ (ε : ℝ), δ < ε → (s ∩ Set.Ioc δ ε).Nonempty<VAR>E : Set α<GOAL>Metric.cthickening δ E = ⋂ ε ∈ s, Metric.thickening ε E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_nn : 0 ≤ δ<VAR>E : Set α<GOAL>Metric.cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), Metric.thickening ε E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>Metric.cthickening δ E = ⋂ ε, ⋂ (_ : max 0 δ < ε), Metric.thickening ε E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Set.Ioc 0 ε).Nonempty<GOAL>closure E = ⋂ δ ∈ s, Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<GOAL>closure E = ⋂ δ, ⋂ (_ : 0 < δ), Metric.cthickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>s : Set ℝ<VAR>hs₀ : s ⊆ Set.Ioi 0<VAR>hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Set.Ioc 0 ε).Nonempty<GOAL>closure E = ⋂ δ ∈ s, Metric.thickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<GOAL>closure E = ⋂ δ, ⋂ (_ : 0 < δ), Metric.thickening δ E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>E : Set α<VAR>δ : ℝ<GOAL>frontier (Metric.cthickening δ E) ⊆ {x | EMetric.infEdist x E = ENNReal.ofReal δ}
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>E : Set α<VAR>hx : x ∈ E<VAR>δ : ℝ<GOAL>Metric.closedBall x δ ⊆ Metric.cthickening δ E
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>E : Set α<VAR>δ δ' : ℝ<VAR>hδ₀ : 0 < δ'<VAR>hδδ' : δ < δ'<GOAL>Metric.cthickening δ E ⊆ ⋃ x ∈ E, Metric.closedBall x δ'
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>hE : IsCompact E<VAR>hδ : 0 ≤ δ<GOAL>Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
<VAR>δ : ℝ<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>E : Set α<VAR>hδ : 0 ≤ δ<GOAL>Metric.cthickening δ E = ⋃ x ∈ closure E, Metric.closedBall x δ
<VAR>δ : ℝ<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>E : Set α<VAR>hE : IsClosed E<VAR>hδ : 0 ≤ δ<GOAL>Metric.cthickening δ E = ⋃ x ∈ E, Metric.closedBall x δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<GOAL>EMetric.infEdist x s ≤ EMetric.infEdist x (Metric.cthickening δ s) + ENNReal.ofReal δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>s : Set α<VAR>x : α<GOAL>EMetric.infEdist x s ≤ EMetric.infEdist x (Metric.thickening δ s) + ENNReal.ofReal δ
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ε δ : ℝ<VAR>s : Set α<GOAL>Metric.thickening ε (Metric.thickening δ s) ⊆ Metric.thickening (ε + δ) s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ : ℝ<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<GOAL>Metric.thickening ε (Metric.cthickening δ s) ⊆ Metric.thickening (ε + δ) s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ε : ℝ<VAR>hε : 0 ≤ ε<VAR>δ : ℝ<VAR>s : Set α<GOAL>Metric.cthickening ε (Metric.thickening δ s) ⊆ Metric.cthickening (ε + δ) s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>hε : 0 ≤ ε<VAR>hδ : 0 ≤ δ<VAR>s : Set α<GOAL>Metric.cthickening ε (Metric.cthickening δ s) ⊆ Metric.cthickening (ε + δ) s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>A : Set α<GOAL>Pairwise (Disjoint on fun r => frontier (Metric.cthickening (↑r) A))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Presheaf C X<VAR>h : F.IsSheaf<GOAL>((TopCat.Presheaf.pushforward C f).obj F).IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>TopCat.Sheaf.pushforward C f ⋙ TopCat.Sheaf.forget C Y = TopCat.Sheaf.forget C X ⋙ TopCat.Presheaf.pushforward C f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F : TopCat.Sheaf C X<GOAL>((TopCat.Sheaf.pushforward C f).obj F).val = (TopCat.Presheaf.pushforward C f).obj F.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : TopCat<VAR>f : X ⟶ Y<VAR>F F' : TopCat.Sheaf C X<VAR>α : F ⟶ F'<GOAL>((TopCat.Sheaf.pushforward C f).map α).val = (TopCat.Presheaf.pushforward C f).map α.val
<VAR>X Y : TopCat<VAR>A : Type u_1<VAR>CategoryTheory.Category.{w, u_1} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.Limits.HasColimits A<VAR>CategoryTheory.Limits.HasLimits A<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)<VAR>(CategoryTheory.forget A).ReflectsIsomorphisms<VAR>f : X ⟶ Y<GOAL>TopCat.Sheaf.pullback A f = TopCat.Sheaf.forget A Y ⋙ TopCat.Presheaf.pullback A f ⋙ CategoryTheory.presheafToSheaf (Opens.grothendieckTopology ↑X) A
<VAR>ε : ℝ<VAR>hε : 0 < ε<GOAL>∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
<VAR>α : Sort u_3<VAR>x y : α<VAR>dist : α → α → ℝ<VAR>dist_self : ∀ (x : α), dist x x = 0<VAR>dist_comm : ∀ (x y : α), dist x y = dist y x<VAR>dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z<GOAL>0 ≤ dist x y
<VAR>α : Type u<VAR>self : PseudoMetricSpace α<VAR>x : α<GOAL>dist x x = 0
<VAR>α : Type u<VAR>self : PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x z ≤ dist x y + dist y z
<VAR>α : Type u<VAR>self : PseudoMetricSpace α<GOAL>𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
<VAR>α : Type u<VAR>self : PseudoMetricSpace α<VAR>x y : α<GOAL>PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
<VAR>α : Type u<VAR>self : PseudoMetricSpace α<VAR>x y : α<GOAL>dist x y = dist y x
<VAR>α : Type u<VAR>self : PseudoMetricSpace α<GOAL>(Bornology.cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
<VAR>α : Type u_3<VAR>m m' : PseudoMetricSpace α<VAR>h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist<GOAL>m = m'
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>dist x x = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>dist x y = dist y x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>edist x y = ENNReal.ofReal (dist x y)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x z ≤ dist x y + dist y z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x y ≤ dist z x + dist z y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x y ≤ dist x z + dist y z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z w : α<GOAL>dist x w ≤ dist x y + dist y z + dist z w
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x₁ y₁ x₂ y₂ : α<GOAL>dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x₁ y₁ x₂ y₂ : α<GOAL>dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>n : ℕ<GOAL>dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, dist (f i) (f (i + 1))
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>d : ℕ → ℝ<VAR>hd : ∀ {k : ℕ}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k<GOAL>dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>d : ℕ → ℝ<VAR>hd : ∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k<GOAL>dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>Function.swap dist = dist
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>|dist x z - dist y z| ≤ dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>0 ≤ dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>a b : α<GOAL>|dist a b| = dist a b
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>dist x y = ↑(nndist x y)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>↑(nndist x y) = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>edist x y = ↑(nndist x y)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>nndist x y = (edist x y).toNNReal
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>↑(nndist x y) = edist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>c : ℝ≥0<GOAL>edist x y < ↑c ↔ nndist x y < c
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>c : ℝ≥0<GOAL>edist x y ≤ ↑c ↔ nndist x y ≤ c
<VAR>α : Type u_3<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>edist x y < ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>edist x y ≠ ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>a : α<GOAL>nndist a a = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>c : ℝ≥0<GOAL>dist x y < ↑c ↔ nndist x y < c
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>c : ℝ≥0<GOAL>dist x y ≤ ↑c ↔ nndist x y ≤ c
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>r : ℝ<GOAL>edist x y < ENNReal.ofReal r ↔ dist x y < r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>nndist x y = (dist x y).toNNReal
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>nndist x y = nndist y x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>nndist x z ≤ nndist x y + nndist y z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>nndist x y ≤ nndist z x + nndist z y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>nndist x y ≤ nndist x z + nndist y z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>dist x y = (edist x y).toReal
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>y ∈ Metric.ball x ε ↔ dist y x < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>y ∈ Metric.ball x ε ↔ dist x y < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<VAR>hy : y ∈ Metric.ball x ε<GOAL>0 < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>h : 0 < ε<GOAL>x ∈ Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>(Metric.ball x ε).Nonempty ↔ 0 < ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.ball x ε = ∅ ↔ ε ≤ 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Metric.ball x 0 = ∅
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<VAR>h : x ∈ Metric.ball y ε<GOAL>∃ ε' < ε, x ∈ Metric.ball y ε'
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ε : ℝ<VAR>x : α<GOAL>UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ε : ℝ<VAR>x : α<GOAL>UniformSpace.ball x {p | dist p.1 p.2 < ε} = Metric.ball x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>⋃ n, Metric.ball x ↑n = Set.univ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>⋃ n, Metric.ball x (↑n + 1) = Set.univ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>y ∈ Metric.closedBall x ε ↔ dist y x ≤ ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>y ∈ Metric.closedBall x ε ↔ dist x y ≤ ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>y ∈ Metric.sphere x ε ↔ dist y x = ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<GOAL>y ∈ Metric.sphere x ε ↔ dist x y = ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<VAR>h : y ∈ Metric.sphere x ε<VAR>hε : ε ≠ 0<GOAL>y ≠ x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>ε : ℝ<VAR>hy : y ∈ Metric.sphere x ε<GOAL>0 ≤ ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>hε : ε < 0<GOAL>Metric.sphere x ε = ∅
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>Subsingleton α<VAR>hε : ε ≠ 0<GOAL>Metric.sphere x ε = ∅
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>h : 0 ≤ ε<GOAL>x ∈ Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>(Metric.closedBall x ε).Nonempty ↔ 0 ≤ ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.closedBall x ε = ∅ ↔ ε < 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<VAR>hε : ε ≤ 0<GOAL>Metric.closedBall x ε = Metric.sphere x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.ball x ε ⊆ Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>Metric.sphere x ε ⊆ Metric.closedBall x ε
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r R : ℝ<VAR>h : r < R<GOAL>Metric.sphere x r ⊆ Metric.ball x R
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>δ ε : ℝ<VAR>h : δ + ε ≤ dist x y<GOAL>Disjoint (Metric.closedBall x δ) (Metric.ball y ε)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>δ ε : ℝ<VAR>h : δ + ε ≤ dist x y<GOAL>Disjoint (Metric.ball x δ) (Metric.closedBall y ε)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<VAR>δ ε : ℝ<VAR>h : δ + ε ≤ dist x y<GOAL>Disjoint (Metric.ball x δ) (Metric.ball y ε)