ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>UniformSpace ι<VAR>CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>UniformInducing (⇑UniformFun.ofFun ∘ F) ↔ UniformInducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>TopologicalSpace ι<VAR>CompactSpace X<VAR>F_eqcont : Equicontinuous F<GOAL>Inducing (⇑UniformFun.ofFun ∘ F) ↔ Inducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>CompactSpace X<VAR>F_eqcont : Equicontinuous F<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Filter.Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f)) ↔ Filter.Tendsto F ℱ (𝓝 f)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ UniformInducing ((⋃₀ 𝔖).restrict ∘ F)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>UniformSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ⋃₀ 𝔖 = Set.univ<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ UniformInducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Inducing ((⋃₀ 𝔖).restrict ∘ F)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_covers : ⋃₀ 𝔖 = Set.univ<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Inducing F
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Filter.Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Filter.Tendsto ((⋃₀ 𝔖).restrict ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict f))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>𝔖_covers : ⋃₀ 𝔖 = Set.univ<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>ℱ : Filter ι<VAR>f : X → α<GOAL>Filter.Tendsto (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ (𝓝 ((UniformOnFun.ofFun 𝔖) f)) ↔ Filter.Tendsto F ℱ (𝓝 f)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>H : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<GOAL>IsClosed (Set.range ((⋃₀ 𝔖).restrict ∘ F))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>𝔖_covers : ⋃₀ 𝔖 = Set.univ<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔ IsClosed (Set.range F)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_ind : Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_cl : IsClosed (Set.range (⇑(UniformOnFun.ofFun 𝔖) ∘ F))<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q<GOAL>CompactSpace ι
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<VAR>F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q<GOAL>CompactSpace ι
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>F : ι → X → α<VAR>TopologicalSpace ι<VAR>T2Space α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>s : Set ι<VAR>s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q<GOAL>IsCompact (closure s)
<VAR>X : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>UniformSpace α<VAR>S : Set C(X, α)<VAR>hS1 : IsCompact (ContinuousMap.toFun '' S)<VAR>hS2 : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact S
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hr : 0 < r<VAR>hs : IsClosed s<VAR>h : s ⊆ Metric.ball x r<GOAL>∃ r' ∈ Set.Ioo 0 r, s ⊆ Metric.ball x r'
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>x : α<VAR>r : ℝ<VAR>s : Set α<VAR>hs : IsClosed s<VAR>h : s ⊆ Metric.ball x r<GOAL>∃ r' < r, s ⊆ Metric.ball x r'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>TopologicalSpace β<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTopology β<VAR>f : α → β<VAR>a z : α<VAR>r : ℝ<VAR>hf : ContinuousOn f (Metric.closedBall a r)<VAR>hz : z ∈ Metric.closedBall a r<VAR>hf1 : ∀ z' ∈ Metric.sphere a r, f z < f z'<GOAL>∃ z ∈ Metric.ball a r, IsLocalMin f z
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<GOAL>Bornology.IsBounded (Metric.closedBall x r)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<GOAL>Bornology.IsBounded (Metric.ball x r)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<GOAL>Bornology.IsBounded (Metric.sphere x r)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>c : α<GOAL>Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.closedBall c r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : Bornology.IsBounded s<VAR>c : α<GOAL>∃ r, s ⊆ Metric.closedBall c r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : Bornology.IsBounded s<VAR>a : ℝ<VAR>c : α<GOAL>∃ r, a < r ∧ s ⊆ Metric.ball c r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : Bornology.IsBounded s<VAR>c : α<GOAL>∃ r, s ⊆ Metric.ball c r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>c : α<GOAL>Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.ball c r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : Bornology.IsBounded s<VAR>a : ℝ<VAR>c : α<GOAL>∃ r, a < r ∧ s ⊆ Metric.closedBall c r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : Bornology.IsBounded s<GOAL>Bornology.IsBounded (closure s)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Bornology.IsBounded (closure s) ↔ Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>c : α<GOAL>(Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.closedBall c r)ᶜ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>c : α<GOAL>(Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.ball c r)ᶜ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>c : α<GOAL>Filter.comap (fun x => dist x c) Filter.atTop = Bornology.cobounded α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>c : α<GOAL>Filter.comap (dist c) Filter.atTop = Bornology.cobounded α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>c : α<VAR>f : β → α<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => dist (f x) c) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded α)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>c : α<VAR>f : β → α<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => dist c (f x)) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded α)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>c : α<GOAL>Filter.Tendsto (fun x => dist x c) (Bornology.cobounded α) Filter.atTop
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>c : α<GOAL>Filter.Tendsto (dist c) (Bornology.cobounded α) Filter.atTop
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : TotallyBounded s<GOAL>Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : IsCompact s<GOAL>Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>Bornology.cobounded α ≤ Filter.cocompact α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>c : α<GOAL>Bornology.IsCobounded s ↔ ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : Bornology.IsCobounded s<VAR>c : α<GOAL>∃ r, (Metric.closedBall c r)ᶜ ⊆ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s ∈ Filter.cocompact α<VAR>c : α<GOAL>∃ r, (Metric.closedBall c r)ᶜ ⊆ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ProperSpace α<VAR>c : α<VAR>h : ∃ r, (Metric.closedBall c r)ᶜ ⊆ s<GOAL>s ∈ Filter.cocompact α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ProperSpace α<VAR>c : α<GOAL>s ∈ Filter.cocompact α ↔ ∃ r, (Metric.closedBall c r)ᶜ ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<GOAL>Bornology.IsBounded (Set.range f) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>s : Set β<GOAL>Bornology.IsBounded (f '' s) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>hf : Filter.Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)<GOAL>Bornology.IsBounded (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>hf : Cauchy (Filter.map f Filter.cofinite)<GOAL>Bornology.IsBounded (Set.range f)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : ℕ → α<VAR>hf : CauchySeq f<GOAL>Bornology.IsBounded (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>a : α<VAR>hf : Filter.Tendsto f Filter.cofinite (𝓝 a)<GOAL>Bornology.IsBounded (Set.range f)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>CompactSpace α<GOAL>Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>u : ℕ → α<VAR>x : α<VAR>hu : Filter.Tendsto u Filter.atTop (𝓝 x)<GOAL>Bornology.IsBounded (Set.range u)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Disjoint (𝓝 x) (Bornology.cobounded α)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Disjoint (Bornology.cobounded α) (𝓝 x)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>Disjoint (𝓝ˢ s) (Bornology.cobounded α)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>Disjoint (Bornology.cobounded α) (𝓝ˢ s)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>PseudoMetricSpace β<VAR>l : Filter α<VAR>f : α → β<VAR>x : β<VAR>hf : Filter.Tendsto f l (𝓝 x)<GOAL>∃ s ∈ l, Bornology.IsBounded (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousWithinAt f s x<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>k : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hf : ∀ x ∈ k, ContinuousAt f x<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hks : k ⊆ s<VAR>hf : ContinuousOn f s<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>TopologicalSpace β<VAR>k s : Set β<VAR>f : β → α<VAR>hk : IsCompact k<VAR>hs : IsOpen s<VAR>hks : k ⊆ s<VAR>hf : ContinuousOn f s<GOAL>∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ProperSpace α<VAR>hc : IsClosed s<VAR>hb : Bornology.IsBounded s<GOAL>IsCompact s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>ProperSpace α<VAR>h : Bornology.IsBounded s<GOAL>IsCompact (closure s)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>T2Space α<VAR>ProperSpace α<GOAL>IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<GOAL>CompactSpace α ↔ Bornology.IsBounded Set.univ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>TotallyBounded (Set.Icc a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>TotallyBounded (Set.Ico a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>TotallyBounded (Set.Ioc a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>TotallyBounded (Set.Ioo a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>Bornology.IsBounded (Set.Icc a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>Bornology.IsBounded (Set.Ico a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>Bornology.IsBounded (Set.Ioc a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>a b : α<GOAL>Bornology.IsBounded (Set.Ioo a b)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Preorder α<VAR>CompactIccSpace α<VAR>s : Set α<VAR>h₁ : BddAbove s<VAR>h₂ : BddBelow s<GOAL>Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>0 ≤ Metric.diam s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>Metric.diam s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>Metric.diam ∅ = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Metric.diam {x} = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>Zero α<GOAL>Metric.diam 0 = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>One α<GOAL>Metric.diam 1 = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>Metric.diam {x, y} = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y z : α<GOAL>Metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>C : ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C<GOAL>EMetric.diam s ≤ ENNReal.ofReal C
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>C : ℝ<VAR>h₀ : 0 ≤ C<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C<GOAL>Metric.diam s ≤ C
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>C : ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C<GOAL>Metric.diam s ≤ C
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>h : EMetric.diam s ≠ ⊤<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>dist x y ≤ Metric.diam s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Bornology.IsBounded s ↔ EMetric.diam s ≠ ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>EMetric.diam s = ⊤ ↔ ¬Bornology.IsBounded s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<GOAL>EMetric.diam Set.univ = ⊤ ↔ NoncompactSpace α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>NoncompactSpace α<GOAL>EMetric.diam Set.univ = ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>NoncompactSpace α<GOAL>Metric.diam Set.univ = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>h : Bornology.IsBounded s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>dist x y ≤ Metric.diam s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : ¬Bornology.IsBounded s<GOAL>EMetric.diam s = ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>h : ¬Bornology.IsBounded s<GOAL>Metric.diam s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : Bornology.IsBounded t<GOAL>Metric.diam s ≤ Metric.diam t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>t : Set α<VAR>xs : x ∈ s<VAR>yt : y ∈ t<GOAL>Metric.diam (s ∪ t) ≤ Metric.diam s + dist x y + Metric.diam t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>h : (s ∩ t).Nonempty<GOAL>Metric.diam (s ∪ t) ≤ Metric.diam s + Metric.diam t
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>h : s ⊆ Metric.closedBall x r<GOAL>Metric.diam s ≤ 2 * r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<VAR>h : 0 ≤ r<GOAL>Metric.diam (Metric.closedBall x r) ≤ 2 * r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<VAR>r : ℝ<VAR>h : 0 ≤ r<GOAL>Metric.diam (Metric.ball x r) ≤ 2 * r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : ℕ → Set α<VAR>h0 : IsComplete (s 0)<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), Bornology.IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (𝓝 0)<GOAL>(⋂ n, s n).Nonempty
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>CompleteSpace α<VAR>s : ℕ → Set α<VAR>hs : ∀ (n : ℕ), IsClosed (s n)<VAR>h's : ∀ (n : ℕ), Bornology.IsBounded (s n)<VAR>h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty<VAR>h' : Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (𝓝 0)<GOAL>(⋂ n, s n).Nonempty
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<GOAL>Bornology.cobounded α = Filter.cocompact α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>x : α<GOAL>Filter.Tendsto (fun x_1 => dist x_1 x) (Filter.cocompact α) Filter.atTop
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>x : α<GOAL>Filter.Tendsto (dist x) (Filter.cocompact α) Filter.atTop
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>x : α<GOAL>Filter.comap (dist x) Filter.atTop = Filter.cocompact α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>f : β → α<VAR>l : Filter β<VAR>x : α<VAR>h : Filter.Tendsto (fun y => dist (f y) x) l Filter.atTop<GOAL>Filter.Tendsto f l (Filter.cocompact α)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>ProperSpace α<VAR>K s : Set α<VAR>DiscreteTopology ↑s<VAR>hK : Bornology.IsBounded K<VAR>hs : IsClosed s<GOAL>(K ∩ s).Finite
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace B<VAR>b : B<GOAL>Trivialization.coordChangeL 𝕜 (Bundle.Trivial.trivialization B F) (Bundle.Trivial.trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>TopologicalSpace B<VAR>F₁ : Type u_3<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → AddCommMonoid (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>(x : B) → AddCommMonoid (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>e₁ e₁' : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear 𝕜 e₁<VAR>Trivialization.IsLinear 𝕜 e₁'<VAR>Trivialization.IsLinear 𝕜 e₂<VAR>Trivialization.IsLinear 𝕜 e₂'<VAR>b : B<VAR>hb : b ∈ (e₁.prod e₂).baseSet ∩ (e₁'.prod e₂').baseSet<GOAL>↑(Trivialization.coordChangeL 𝕜 (e₁.prod e₂) (e₁'.prod e₂') b) = (↑(Trivialization.coordChangeL 𝕜 e₁ e₁' b)).prodMap ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>TopologicalSpace B<VAR>F₁ : Type u_3<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → AddCommMonoid (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>(x : B) → AddCommMonoid (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₁ E₁<VAR>FiberBundle F₂ E₂<VAR>Trivialization.IsLinear 𝕜 e₁<VAR>Trivialization.IsLinear 𝕜 e₂<VAR>x : B<VAR>hx₁ : x ∈ e₁.baseSet<VAR>hx₂ : x ∈ e₂.baseSet<VAR>v₁ : E₁ x<VAR>v₂ : E₂ x<GOAL>↑(e₁.prod e₂) { proj := x, snd := (v₁, v₂) } = (x, (Trivialization.continuousLinearEquivAt 𝕜 e₁ x hx₁) v₁, (Trivialization.continuousLinearEquivAt 𝕜 e₂ x hx₂) v₂)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>TopologicalSpace B<VAR>F₁ : Type u_3<VAR>NormedAddCommGroup F₁<VAR>NormedSpace 𝕜 F₁<VAR>E₁ : B → Type u_4<VAR>TopologicalSpace (Bundle.TotalSpace F₁ E₁)<VAR>F₂ : Type u_5<VAR>NormedAddCommGroup F₂<VAR>NormedSpace 𝕜 F₂<VAR>E₂ : B → Type u_6<VAR>TopologicalSpace (Bundle.TotalSpace F₂ E₂)<VAR>(x : B) → AddCommMonoid (E₁ x)<VAR>(x : B) → Module 𝕜 (E₁ x)<VAR>(x : B) → AddCommMonoid (E₂ x)<VAR>(x : B) → Module 𝕜 (E₂ x)<VAR>(x : B) → TopologicalSpace (E₁ x)<VAR>(x : B) → TopologicalSpace (E₂ x)<VAR>FiberBundle F₁ E₁<VAR>FiberBundle F₂ E₂<VAR>e₁ : Trivialization F₁ Bundle.TotalSpace.proj<VAR>e₂ : Trivialization F₂ Bundle.TotalSpace.proj<VAR>Trivialization.IsLinear 𝕜 e₁<VAR>Trivialization.IsLinear 𝕜 e₂<VAR>x : B<VAR>hx : x ∈ (e₁.prod e₂).baseSet<GOAL>Trivialization.continuousLinearEquivAt 𝕜 (e₁.prod e₂) x hx = (Trivialization.continuousLinearEquivAt 𝕜 e₁ x ⋯).prod (Trivialization.continuousLinearEquivAt 𝕜 e₂ x ⋯)
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>p : α → Prop<VAR>x y : Subtype p<GOAL>dist x y = dist ↑x ↑y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>p : α → Prop<VAR>x y : Subtype p<GOAL>nndist x y = nndist ↑x ↑y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : αᵃᵒᵖ<GOAL>dist (AddOpposite.unop x) (AddOpposite.unop y) = dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : αᵐᵒᵖ<GOAL>dist (MulOpposite.unop x) (MulOpposite.unop y) = dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>dist (AddOpposite.op x) (AddOpposite.op y) = dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>dist (MulOpposite.op x) (MulOpposite.op y) = dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : αᵃᵒᵖ<GOAL>nndist (AddOpposite.unop x) (AddOpposite.unop y) = nndist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : αᵐᵒᵖ<GOAL>nndist (MulOpposite.unop x) (MulOpposite.unop y) = nndist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>nndist (AddOpposite.op x) (AddOpposite.op y) = nndist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>nndist (MulOpposite.op x) (MulOpposite.op y) = nndist x y
<VAR>a b : ℝ≥0<GOAL>dist a b = |↑a - ↑b|
<VAR>a b : ℝ≥0<GOAL>nndist a b = max (a - b) (b - a)
<VAR>z : ℝ≥0<GOAL>nndist 0 z = z
<VAR>z : ℝ≥0<GOAL>nndist z 0 = z
<VAR>a b : ℝ≥0<GOAL>a ≤ b + nndist a b
<VAR>c : ℝ≥0<GOAL>Metric.ball 0 ↑c = Set.Ico 0 c
<VAR>c : ℝ<GOAL>Metric.ball 0 c = Set.Ico 0 c.toNNReal
<VAR>c : ℝ≥0<GOAL>Metric.closedBall 0 ↑c = Set.Icc 0 c
<VAR>c : ℝ<VAR>c_nn : 0 ≤ c<GOAL>Metric.closedBall 0 c = Set.Icc 0 c.toNNReal
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>x y : ULift.{u_3, u_2} β<GOAL>dist x y = dist x.down y.down
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>x y : ULift.{u_3, u_2} β<GOAL>nndist x y = nndist x.down y.down
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>x y : β<GOAL>dist { down := x } { down := y } = dist x y
<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>x y : β<GOAL>nndist { down := x } { down := y } = nndist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x y : α × β<GOAL>dist x y = max (dist x.1 y.1) (dist x.2 y.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x : α<VAR>y₁ y₂ : β<GOAL>dist (x, y₁) (x, y₂) = dist y₁ y₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x₁ x₂ : α<VAR>y : β<GOAL>dist (x₁, y) (x₂, y) = dist x₁ x₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ<GOAL>Metric.ball x r ×ˢ Metric.ball y r = Metric.ball (x, y) r