ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>LocallyCompactSpace X<VAR>x : X<GOAL>∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>ι : Sort u_2<VAR>c : ι → Set X<VAR>s : Set X<VAR>hs : IsSeqCompact s<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : s ⊆ ⋃ i, c i<GOAL>∃ δ > 0, ∀ a ∈ s, ∃ i, Metric.ball a δ ⊆ c i
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>ProperSpace X<VAR>s : Set X<VAR>hs : Bornology.IsBounded s<VAR>x : ℕ → X<VAR>hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s<GOAL>∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>ProperSpace X<VAR>s : Set X<VAR>hs : Bornology.IsBounded s<VAR>x : ℕ → X<VAR>hx : ∀ (n : ℕ), x n ∈ s<GOAL>∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>self : UniformInducing f<GOAL>Filter.comap (fun x => (f x.1, f x.2)) (𝓤 β) = 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformInducing f ↔ Filter.comap (fun x => (f x.1, f x.2)) (𝓤 β) = 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformInducing f ↔ UniformSpace.comap f inst✝ = inst✝¹
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>p : ι → Prop<VAR>p' : ι' → Prop<VAR>s : ι → Set (α × α)<VAR>s' : ι' → Set (β × β)<VAR>h : (𝓤 α).HasBasis p s<VAR>h' : (𝓤 β).HasBasis p' s'<VAR>f : α → β<GOAL>UniformInducing f ↔ (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s<GOAL>UniformInducing f
<VAR>α : Type u<VAR>UniformSpace α<GOAL>UniformInducing id
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformInducing g<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>UniformInducing (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformInducing g<VAR>f : α → β<GOAL>UniformInducing (g ∘ f) ↔ UniformInducing f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformInducing f<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>H : (𝓤 β).HasBasis p s<GOAL>(𝓤 α).HasBasis p fun i => Prod.map f f ⁻¹' s i
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformInducing f<VAR>F : Filter α<GOAL>Cauchy (Filter.map f F) ↔ Cauchy F
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>hgf : UniformInducing (g ∘ f)<GOAL>UniformInducing f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>UniformContinuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : UniformInducing g<GOAL>UniformContinuous f ↔ UniformContinuous (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : UniformInducing g<GOAL>UniformInducing (g ∘ f) ↔ UniformInducing f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>S : Set α<VAR>hg : UniformInducing g<GOAL>UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : UniformInducing f<GOAL>Inducing f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>UniformSpace α'<VAR>UniformSpace β'<VAR>e₁ : α → α'<VAR>e₂ : β → β'<VAR>h₁ : UniformInducing e₁<VAR>h₂ : UniformInducing e₂<GOAL>UniformInducing fun p => (e₁ p.1, e₂ p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : UniformInducing f<VAR>hd : DenseRange f<GOAL>DenseInducing f
<VAR>α : Type u<VAR>UniformSpace α<GOAL>UniformInducing SeparationQuotient.mk
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>T0Space α<VAR>f : α → β<VAR>h : UniformInducing f<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>self : UniformEmbedding f<GOAL>Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformEmbedding f ↔ UniformInducing f ∧ Function.Injective f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>p : ι → Prop<VAR>p' : ι' → Prop<VAR>s : ι → Set (α × α)<VAR>s' : ι' → Set (β × β)<VAR>h : (𝓤 α).HasBasis p s<VAR>h' : (𝓤 β).HasBasis p' s'<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Function.Injective f ∧ (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>p : ι → Prop<VAR>p' : ι' → Prop<VAR>s : ι → Set (α × α)<VAR>s' : ι' → Set (β × β)<VAR>h : (𝓤 α).HasBasis p s<VAR>h' : (𝓤 β).HasBasis p' s'<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
<VAR>α : Type u<VAR>UniformSpace α<VAR>p : α → Prop<GOAL>UniformEmbedding Subtype.val
<VAR>α : Type u<VAR>UniformSpace α<VAR>s t : Set α<VAR>hst : s ⊆ t<GOAL>UniformEmbedding (Set.inclusion hst)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformEmbedding g<VAR>f : α → β<VAR>hf : UniformEmbedding f<GOAL>UniformEmbedding (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformEmbedding g<VAR>f : α → β<GOAL>UniformEmbedding (g ∘ f) ↔ UniformEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α ≃ β<VAR>h₁ : UniformContinuous ⇑f<VAR>h₂ : UniformContinuous ⇑f.symm<GOAL>UniformEmbedding ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformEmbedding Sum.inl
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<GOAL>UniformEmbedding Sum.inr
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>T0Space α<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>UniformEmbedding f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>T0Space α<VAR>f : α → β<GOAL>UniformEmbedding f ↔ UniformInducing f
<VAR>β : Type v<VAR>UniformSpace β<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>Filter.comap (Prod.map f f) (𝓤 β) = 𝓟 idRel
<VAR>β : Type v<VAR>UniformSpace β<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>UniformEmbedding f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : UniformEmbedding f<GOAL>Embedding f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>h : UniformEmbedding f<VAR>hd : DenseRange f<GOAL>DenseEmbedding f
<VAR>β : Type v<VAR>UniformSpace β<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>T0Space β<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>ClosedEmbedding f
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>s : Set (α × α)<VAR>e : α → β<VAR>b : β<VAR>he₁ : UniformInducing e<VAR>he₂ : DenseInducing e<VAR>hs : s ∈ 𝓤 α<GOAL>∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>p : α → Prop<VAR>e : α → β<VAR>ue : UniformEmbedding e<VAR>de : DenseEmbedding e<GOAL>UniformEmbedding (DenseEmbedding.subtypeEmb p e)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>UniformSpace α'<VAR>UniformSpace β'<VAR>e₁ : α → α'<VAR>e₂ : β → β'<VAR>h₁ : UniformEmbedding e₁<VAR>h₂ : UniformEmbedding e₂<GOAL>UniformEmbedding fun p => (e₁ p.1, e₂ p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>m : α → β<VAR>s : Set α<VAR>hm : UniformInducing m<GOAL>IsComplete (m '' s) ↔ IsComplete s
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>CompleteSpace α ↔ IsComplete (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>CompleteSpace α<VAR>f : α → β<VAR>hf : UniformInducing f<GOAL>IsComplete (Set.range f)
<VAR>α : Type u<VAR>UniformSpace α<GOAL>CompleteSpace (SeparationQuotient α) ↔ CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>e : α ≃ β<VAR>he : UniformEmbedding ⇑e<GOAL>CompleteSpace α ↔ CompleteSpace β
<VAR>α : Type u<VAR>UniformSpace α<VAR>s : Set α<GOAL>CompleteSpace ↑s ↔ IsComplete s
<VAR>α : Type u<VAR>UniformSpace α<VAR>CompleteSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>CompleteSpace ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>m : β → α<VAR>hm : UniformInducing m<VAR>dense : DenseRange m<VAR>h : ∀ (f : Filter β), Cauchy f → ∃ x, Filter.map m f ≤ 𝓝 x<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : UniformInducing f<GOAL>TotallyBounded (f '' s) ↔ TotallyBounded s
<VAR>α : Type u<VAR>β : Type v<VAR>UniformSpace α<VAR>UniformSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hf : UniformInducing f<VAR>hs : TotallyBounded s<GOAL>TotallyBounded (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>u : UniformSpace β<VAR>hf : Function.Injective f<GOAL>UniformEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>u : UniformSpace β<VAR>f : α → β<VAR>h : Embedding f<GOAL>UniformEmbedding f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>CompleteSpace γ<VAR>a : α<GOAL>∃ c, Filter.Tendsto f (Filter.comap e (𝓝 a)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>CompleteSpace γ<VAR>p : α → Prop<VAR>e : α → β<VAR>f : α → γ<VAR>b : β<VAR>s : Set α<VAR>hf : UniformContinuous fun x => f ↑x<VAR>he : UniformEmbedding e<VAR>hd : ∀ (x : β), x ∈ closure (Set.range e)<VAR>hb : closure (e '' s) ∈ 𝓝 b<VAR>hs : IsClosed s<VAR>hp : ∀ x ∈ s, p x<GOAL>∃ c, Filter.Tendsto f (Filter.comap e (𝓝 b)) (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>CompleteSpace γ<VAR>a : α<GOAL>Filter.Tendsto f (Filter.comap e (𝓝 a)) (𝓝 (⋯.extend f a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>CompleteSpace γ<GOAL>UniformContinuous (⋯.extend f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>h_f : UniformContinuous f<VAR>T0Space γ<VAR>b : β<GOAL>⋯.extend f (e b) = f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>UniformSpace α<VAR>UniformSpace β<VAR>UniformSpace γ<VAR>e : β → α<VAR>h_e : UniformInducing e<VAR>h_dense : DenseRange e<VAR>f : β → γ<VAR>T0Space γ<VAR>g : α → γ<VAR>hg : ∀ (b : β), g (e b) = f b<VAR>hc : Continuous g<GOAL>⋯.extend f = g
<VAR>X : Type u_2<VAR>Dist X<VAR>self : IsUltrametricDist X<VAR>x y z : X<GOAL>dist x z ≤ max (dist x y) (dist y z)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y z : X<GOAL>dist x z ≤ max (dist x y) (dist y z)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r : ℝ<VAR>h : y ∈ Metric.ball x r<GOAL>Metric.ball x r = Metric.ball y r
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r : ℝ<GOAL>y ∈ Metric.ball x r ↔ x ∈ Metric.ball y r
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r s : ℝ<GOAL>Metric.ball x r ⊆ Metric.ball y s ∨ Metric.ball y s ⊆ Metric.ball x r ∨ Disjoint (Metric.ball x r) (Metric.ball y s)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r : ℝ<GOAL>Metric.ball x r = Metric.ball y r ∨ Disjoint (Metric.ball x r) (Metric.ball y r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r : ℝ<VAR>h : y ∈ Metric.closedBall x r<GOAL>Metric.closedBall x r = Metric.closedBall y r
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r : ℝ<GOAL>y ∈ Metric.closedBall x r ↔ x ∈ Metric.closedBall y r
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r s : ℝ<GOAL>Metric.closedBall x r ⊆ Metric.closedBall y s ∨ Metric.closedBall y s ⊆ Metric.closedBall x r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y s)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<GOAL>IsClosed (Metric.ball x r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<GOAL>IsClopen (Metric.ball x r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<GOAL>frontier (Metric.ball x r) = ∅
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x y : X<VAR>r : ℝ<GOAL>Metric.closedBall x r = Metric.closedBall y r ∨ Disjoint (Metric.closedBall x r) (Metric.closedBall y r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>IsOpen (Metric.closedBall x r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>IsClopen (Metric.closedBall x r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (Metric.closedBall x r) = ∅
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>IsOpen (Metric.sphere x r)
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>IsUltrametricDist X<VAR>x : X<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>IsClopen (Metric.sphere x r)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<GOAL>LipschitzWith K f
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<GOAL>0 < 1 - ↑K
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<GOAL>1 - ↑K ≠ 0
<VAR>K : ℝ≥0<GOAL>1 - ↑K ≠ ⊤
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>h : edist x y ≠ ⊤<GOAL>edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>h : edist x y ≠ ⊤<VAR>hy : Function.IsFixedPt f y<GOAL>edist x y ≤ edist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>hx : Function.IsFixedPt f x<VAR>hy : Function.IsFixedPt f y<GOAL>x = y ∨ edist x y = ⊤
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>s : Set α<VAR>hs : Set.MapsTo f s s<GOAL>ContractingWith K (Set.MapsTo.restrict f s s hs)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>∃ y, Function.IsFixedPt f y ∧ Filter.Tendsto (fun n => f^[n] x) Filter.atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>Function.IsFixedPt f (ContractingWith.efixedPoint f hf x hx)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>Filter.Tendsto (fun n => f^[n] x) Filter.atTop (𝓝 (ContractingWith.efixedPoint f hf x hx))
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<VAR>n : ℕ<GOAL>edist (f^[n] x) (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (ContractingWith.efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (ContractingWith.efixedPoint f hf x hx) < ⊤
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>hx : edist x (f x) ≠ ⊤<VAR>y : α<VAR>hy : edist y (f y) ≠ ⊤<VAR>h : edist x y ≠ ⊤<GOAL>ContractingWith.efixedPoint f hf x hx = ContractingWith.efixedPoint f hf y hy
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>∃ y ∈ s, Function.IsFixedPt f y ∧ Filter.Tendsto (fun n => f^[n] x) Filter.atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>ContractingWith.efixedPoint' f hsc hsf hf x hxs hx ∈ s
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>Function.IsFixedPt f (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>Filter.Tendsto (fun n => f^[n] x) Filter.atTop (𝓝 (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx))
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>n : ℕ<GOAL>edist (f^[n] x) (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hf : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<GOAL>edist x (ContractingWith.efixedPoint' f hsc hsf hf x hxs hx) < ⊤
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>s : Set α<VAR>hsc : IsComplete s<VAR>hsf : Set.MapsTo f s s<VAR>hfs : ContractingWith K (Set.MapsTo.restrict f s s hsf)<VAR>x : α<VAR>hxs : x ∈ s<VAR>hx : edist x (f x) ≠ ⊤<VAR>t : Set α<VAR>htc : IsComplete t<VAR>htf : Set.MapsTo f t t<VAR>hft : ContractingWith K (Set.MapsTo.restrict f t t htf)<VAR>y : α<VAR>hyt : y ∈ t<VAR>hy : edist y (f y) ≠ ⊤<VAR>hxy : edist x y ≠ ⊤<GOAL>ContractingWith.efixedPoint' f hsc hsf hfs x hxs hx = ContractingWith.efixedPoint' f htc htf hft y hyt hy
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<GOAL>0 < 1 - ↑K
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<GOAL>dist (f x) (f y) ≤ ↑K * dist x y
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<GOAL>dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x : α<VAR>y : α<VAR>hy : Function.IsFixedPt f y<GOAL>dist x y ≤ dist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>x y : α<VAR>hx : Function.IsFixedPt f x<VAR>hy : Function.IsFixedPt f y<GOAL>x = y
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>g : α → α<VAR>x y : α<VAR>hx : Function.IsFixedPt f x<VAR>hy : Function.IsFixedPt g y<VAR>C : ℝ<VAR>hfg : ∀ (z : α), dist (f z) (g z) ≤ C<GOAL>dist x y ≤ C / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<GOAL>Function.IsFixedPt f (ContractingWith.fixedPoint f hf)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<VAR>x : α<VAR>hx : Function.IsFixedPt f x<GOAL>x = ContractingWith.fixedPoint f hf
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<VAR>x : α<GOAL>dist x (ContractingWith.fixedPoint f hf) ≤ dist x (f x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) (ContractingWith.fixedPoint f hf) ≤ dist x (f x) * ↑K ^ n / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<VAR>x : α<GOAL>Filter.Tendsto (fun n => f^[n] x) Filter.atTop (𝓝 (ContractingWith.fixedPoint f hf))
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>Nonempty α<VAR>CompleteSpace α<VAR>g : α → α<VAR>hg : ContractingWith K g<VAR>C : ℝ<VAR>hfg : ∀ (z : α), dist (f z) (g z) ≤ C<GOAL>dist (ContractingWith.fixedPoint f hf) (ContractingWith.fixedPoint g hg) ≤ C / (1 - ↑K)
<VAR>α : Type u_1<VAR>MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>Nonempty α<VAR>CompleteSpace α<VAR>n : ℕ<VAR>hf : ContractingWith K f^[n]<GOAL>Function.IsFixedPt f (ContractingWith.fixedPoint f^[n] hf)
<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<GOAL>UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i => α)