ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>↑e.symm (proj x, (↑e x).2) = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e e' : Trivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).source = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e e' : Trivialization F proj<GOAL>(e.symm.trans e'.toPartialEquiv).target = (e.baseSet ∩ e'.baseSet) ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>Prod.fst ∘ ↑e =ᶠ[𝓝 x] proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : proj x ∈ e.baseSet<GOAL>Prod.fst ∘ ↑e =ᶠ[𝓝 x] proj
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>Filter.map proj (𝓝 x) = 𝓝 (proj x)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set B<VAR>hb : s ⊆ e.baseSet<GOAL>proj ⁻¹' s ⊆ e.source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set B<VAR>hb : s ⊆ e.baseSet<GOAL>↑e '' (proj ⁻¹' s) = s ×ˢ Set.univ
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>α : Type u_6<VAR>l : Filter α<VAR>f : α → Z<VAR>z : Z<VAR>hz : z ∈ e.source<GOAL>Filter.Tendsto f l (𝓝 z) ↔ Filter.Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Filter.Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>z : Z<VAR>hz : z ∈ e.source<GOAL>𝓝 z = Filter.comap proj (𝓝 (proj z)) ⊓ Filter.comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set B<VAR>hb : s ⊆ e.baseSet<VAR>p : ↑(proj ⁻¹' s)<GOAL>(e.preimageHomeomorph hb) p = (⟨proj ↑p, ⋯⟩, (↑e ↑p).2)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set B<VAR>hb : s ⊆ e.baseSet<VAR>p : ↑s × F<GOAL>(e.preimageHomeomorph hb).symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>p : ↑e.source<GOAL>e.sourceHomeomorphBaseSetProd p = (⟨proj ↑p, ⋯⟩, (↑e ↑p).2)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>p : ↑e.baseSet × F<GOAL>e.sourceHomeomorphBaseSetProd.symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>p : ↑(proj ⁻¹' {b})<GOAL>(e.preimageSingletonHomeomorph hb) p = (↑e ↑p).2
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>p : F<GOAL>(e.preimageSingletonHomeomorph hb).symm p = ⟨↑e.symm (b, p), ⋯⟩
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>x : Z<VAR>ex : x ∈ e.source<GOAL>ContinuousAt proj x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>f : Z → X<VAR>z : Z<VAR>e : Trivialization F proj<VAR>he : proj z ∈ e.baseSet<VAR>hf : ContinuousAt (f ∘ ↑e.symm) (↑e z)<GOAL>ContinuousAt f z
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>X : Type u_6<VAR>TopologicalSpace X<VAR>f : X → Z<VAR>x : X<VAR>e : Trivialization F proj<VAR>hf_proj : ContinuousAt (proj ∘ f) x<VAR>he : proj (f x) ∈ e.baseSet<VAR>hf : ContinuousAt (↑e ∘ f) x<GOAL>ContinuousAt f x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>e' : Trivialization F Bundle.TotalSpace.proj<GOAL>ContinuousOn (↑e') e'.source
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>e' : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>y : E b<GOAL>{ proj := b, snd := y } ∈ e'.source ↔ b ∈ e'.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>e' : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>y : E b<VAR>hb : b ∈ e'.baseSet<GOAL>(↑e' { proj := b, snd := y }).1 = b
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>e' : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>y : F<GOAL>(b, y) ∈ e'.target ↔ b ∈ e'.baseSet
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>e' : Trivialization F Bundle.TotalSpace.proj<VAR>x : Bundle.TotalSpace F E<VAR>hx : x ∈ e'.source<GOAL>↑e'.symm (↑e' x) = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>x : B<VAR>y : F<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>h : x ∈ e.baseSet<GOAL>(↑e.symm (x, y)).proj = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>e.symm b y = cast ⋯ (↑e.symm (b, y)).snd
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∉ e.baseSet<VAR>y : F<GOAL>e.symm b y = 0
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>{ proj := b, snd := e.symm b y } = ↑e.symm (b, y)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>z : Bundle.TotalSpace F E<VAR>hz : z.proj ∈ e.baseSet<GOAL>e.symm z.proj (↑e z).2 = z.snd
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : E b<GOAL>e.symm b (↑e { proj := b, snd := y }).2 = y
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<VAR>b : B<VAR>hb : b ∈ e.baseSet<VAR>y : F<GOAL>↑e { proj := b, snd := e.symm b y } = (b, y)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>TopologicalSpace (Bundle.TotalSpace F E)<VAR>(x : B) → Zero (E x)<VAR>e : Trivialization F Bundle.TotalSpace.proj<GOAL>ContinuousOn (fun z => Bundle.TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ Set.univ)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>F' : Type u_6<VAR>TopologicalSpace F'<VAR>e : Trivialization F proj<VAR>h : F ≃ₜ F'<VAR>x : Z<GOAL>↑(e.transFiberHomeomorph h) x = ((↑e x).1, h (↑e x).2)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>(b, e₁.coordChange e₂ b x) = ↑e₂ (↑e₁.symm (b, x))
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e₁ e₂ : Trivialization F proj<VAR>p : Z<VAR>h : proj p ∈ e₁.baseSet<GOAL>e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>b : B<VAR>h : b ∈ e.baseSet<VAR>x : F<GOAL>e.coordChange e b x = x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>b : B<VAR>h : b ∈ e.baseSet<GOAL>e.coordChange e b = id
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e₁ e₂ e₃ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<VAR>x : F<GOAL>e₂.coordChange e₃ b (e₁.coordChange e₂ b x) = e₁.coordChange e₃ b x
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<GOAL>Continuous (e₁.coordChange e₂ b)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e₁ e₂ : Trivialization F proj<VAR>b : B<VAR>h₁ : b ∈ e₁.baseSet<VAR>h₂ : b ∈ e₂.baseSet<GOAL>⇑(e₁.coordChangeHomeomorph e₂ h₁ h₂) = e₁.coordChange e₂ b
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set B<GOAL>e.IsImage (proj ⁻¹' s) (s ×ˢ Set.univ)
<VAR>B : Type u_2<VAR>F : Type u_3<VAR>Z : Type u_5<VAR>TopologicalSpace B<VAR>TopologicalSpace F<VAR>proj : Z → B<VAR>TopologicalSpace Z<VAR>e : Trivialization F proj<VAR>s : Set B<GOAL>e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofiltered J<VAR>F : CategoryTheory.Functor J Profinite<VAR>C : CategoryTheory.Limits.Cone F<VAR>U : Set ↑C.pt.toTop<VAR>hC : CategoryTheory.Limits.IsLimit C<VAR>hU : IsClopen U<GOAL>∃ j V, IsClopen V ∧ U = ⇑(C.π.app j) ⁻¹' V
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofiltered J<VAR>F : CategoryTheory.Functor J Profinite<VAR>C : CategoryTheory.Limits.Cone F<VAR>hC : CategoryTheory.Limits.IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) (Fin 2)<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofiltered J<VAR>F : CategoryTheory.Functor J Profinite<VAR>C : CategoryTheory.Limits.Cone F<VAR>α : Type u_1<VAR>Finite α<VAR>hC : CategoryTheory.Limits.IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<GOAL>∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofiltered J<VAR>F : CategoryTheory.Functor J Profinite<VAR>C : CategoryTheory.Limits.Cone F<VAR>α : Type u_1<VAR>Finite α<VAR>Nonempty α<VAR>hC : CategoryTheory.Limits.IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofiltered J<VAR>F : CategoryTheory.Functor J Profinite<VAR>C : CategoryTheory.Limits.Cone F<VAR>α : Type u_1<VAR>hC : CategoryTheory.Limits.IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>x y z : ℝ<VAR>h : y ∈ Set.uIcc x z<GOAL>dist x y ≤ dist x z
<VAR>x y z : ℝ<VAR>h : y ∈ Set.uIcc x z<GOAL>dist y z ≤ dist x z
<VAR>x y x' y' : ℝ<VAR>hx : x ∈ Set.uIcc x' y'<VAR>hy : y ∈ Set.uIcc x' y'<GOAL>dist x y ≤ dist x' y'
<VAR>x y x' y' : ℝ<VAR>hx : x ∈ Set.Icc x' y'<VAR>hy : y ∈ Set.Icc x' y'<GOAL>dist x y ≤ y' - x'
<VAR>x y : ℝ<VAR>hx : x ∈ Set.Icc 0 1<VAR>hy : y ∈ Set.Icc 0 1<GOAL>dist x y ≤ 1
<VAR>b : ℝ<GOAL>{b} = ⋂ r, ⋂ (_ : r > 0), Set.Icc (b - r) (b + r)
<VAR>α : Type u_3<VAR>f g : α → ℝ<VAR>t₀ : Filter α<VAR>hf : ∀ᶠ (t : α) in t₀, 0 ≤ f t<VAR>hft : ∀ᶠ (t : α) in t₀, f t ≤ g t<VAR>g0 : Filter.Tendsto g t₀ (𝓝 0)<GOAL>Filter.Tendsto f t₀ (𝓝 0)
<VAR>α : Type u_3<VAR>f g : α → ℝ<VAR>t₀ : Filter α<VAR>hf : ∀ (t : α), 0 ≤ f t<VAR>hft : ∀ (t : α), f t ≤ g t<VAR>g0 : Filter.Tendsto g t₀ (𝓝 0)<GOAL>Filter.Tendsto f t₀ (𝓝 0)
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>u : Set α<VAR>hu : u ∈ 𝓝 x<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, Metric.closedBall x r ⊆ u
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Filter.Tendsto (Metric.closedBall x) (𝓝 0) (𝓝 x).smallSets
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>IsClosed (Metric.closedBall x ε)
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>IsClosed (Metric.sphere x ε)
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>closure (Metric.closedBall x ε) = Metric.closedBall x ε
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>closure (Metric.sphere x ε) = Metric.sphere x ε
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>closure (Metric.ball x ε) ⊆ Metric.closedBall x ε
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>frontier (Metric.ball x ε) ⊆ Metric.sphere x ε
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<VAR>ε : ℝ<GOAL>frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Metric.closedBall x 0 = closure {x}
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>WeaklyLocallyCompactSpace α<VAR>x : α<GOAL>∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (Metric.closedBall x r)
<VAR>α : Type u_2<VAR>PseudoMetricSpace α<VAR>WeaklyLocallyCompactSpace α<VAR>x : α<GOAL>∃ r, 0 < r ∧ IsCompact (Metric.closedBall x r)
<VAR>ι : Type u_1<VAR>Fintype ι<VAR>x y x' y' : ι → ℝ<VAR>hx : x ∈ Set.Icc x' y'<VAR>hy : y ∈ Set.Icc x' y'<GOAL>dist x y ≤ dist x' y'
<VAR>α : Type u<VAR>self : MetricSpace α<VAR>x y : α<GOAL>dist x y = 0 → x = y
<VAR>α : Type u_3<VAR>m m' : MetricSpace α<VAR>h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist<GOAL>m = m'
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>dist x y = 0 → x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>dist x y = 0 ↔ x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>0 = dist x y ↔ x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>dist x y ≠ 0 ↔ x ≠ y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>dist x y ≤ 0 ↔ x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>0 < dist x y ↔ x ≠ y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<VAR>h : ∀ ε > 0, dist x y ≤ ε<GOAL>x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>nndist x y = 0 → x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>nndist x y = 0 ↔ x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x y : γ<GOAL>0 = nndist x y ↔ x = y
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x : γ<GOAL>Metric.closedBall x 0 = {x}
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x : γ<GOAL>Metric.sphere x 0 = {x}
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x : γ<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>(Metric.closedBall x r).Subsingleton
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>x : γ<VAR>r : ℝ<VAR>hr : r ≤ 0<GOAL>(Metric.sphere x r).Subsingleton
<VAR>β : Type v<VAR>γ : Type w<VAR>MetricSpace γ<VAR>MetricSpace β<VAR>f : γ → β<GOAL>UniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>s : Set γ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hs : s.Pairwise fun x y => ε ≤ dist x y<GOAL>IsClosed s
<VAR>γ : Type w<VAR>MetricSpace γ<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>f : α → γ<VAR>hf : Pairwise fun x y => ε ≤ dist (f x) (f y)<GOAL>ClosedEmbedding f
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>β : Type u_3<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>f : β → α<VAR>hf : Pairwise fun x y => ε ≤ dist (f x) (f y)<GOAL>UniformEmbedding f
<VAR>γ : Type u_3<VAR>U : UniformSpace γ<VAR>m : MetricSpace γ<VAR>H : 𝓤 γ = 𝓤 γ<GOAL>m.replaceUniformity H = m
<VAR>γ : Type u_3<VAR>U : TopologicalSpace γ<VAR>m : MetricSpace γ<VAR>H : U = UniformSpace.toTopologicalSpace<GOAL>m.replaceTopology H = m
<VAR>α : Type u_3<VAR>m : MetricSpace α<VAR>B : Bornology α<VAR>H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s<GOAL>m.replaceBornology H = m
<VAR>α : Type u<VAR>MetricSpace α<VAR>H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>p q : α<GOAL>dist (SeparationQuotient.mk p) (SeparationQuotient.mk q) = dist p q
<VAR>X : Type u_1<VAR>Dist X<VAR>a b : X<GOAL>dist (Additive.ofMul a) (Additive.ofMul b) = dist a b
<VAR>X : Type u_1<VAR>Dist X<VAR>a b : X<GOAL>dist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = dist a b
<VAR>X : Type u_1<VAR>Dist X<VAR>a b : Additive X<GOAL>dist (Additive.toMul a) (Additive.toMul b) = dist a b
<VAR>X : Type u_1<VAR>Dist X<VAR>a b : Multiplicative X<GOAL>dist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = dist a b
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>a b : X<GOAL>nndist (Additive.ofMul a) (Additive.ofMul b) = nndist a b
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>a b : X<GOAL>nndist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = nndist a b
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>a b : Additive X<GOAL>nndist (Additive.toMul a) (Additive.toMul b) = nndist a b
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>a b : Multiplicative X<GOAL>nndist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = nndist a b
<VAR>X : Type u_1<VAR>Dist X<VAR>a b : X<GOAL>dist (OrderDual.toDual a) (OrderDual.toDual b) = dist a b
<VAR>X : Type u_1<VAR>Dist X<VAR>a b : Xᵒᵈ<GOAL>dist (OrderDual.ofDual a) (OrderDual.ofDual b) = dist a b
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>a b : X<GOAL>nndist (OrderDual.toDual a) (OrderDual.toDual b) = nndist a b
<VAR>X : Type u_1<VAR>PseudoMetricSpace X<VAR>a b : Xᵒᵈ<GOAL>nndist (OrderDual.ofDual a) (OrderDual.ofDual b) = nndist a b
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>self : Urysohns.CU P<GOAL>IsOpen self.U
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>self : Urysohns.CU P<GOAL>self.C ⊆ self.U
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>self : Urysohns.CU P<GOAL>P self.C
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>self : Urysohns.CU P<VAR>c u : Set X<GOAL>IsClosed c → P c → IsOpen u → c ⊆ u → ∃ v, IsOpen v ∧ c ⊆ v ∧ closure v ⊆ u ∧ P (closure v)
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>self : Urysohns.CU P<GOAL>IsClosed self.C
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<GOAL>c.left.C = c.C
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<GOAL>c.right.U = c.U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<GOAL>c.left.U ⊆ c.right.C
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<GOAL>c.left.U ⊆ c.U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<GOAL>c.C ⊆ c.right.C
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>n : ℕ<VAR>x : X<VAR>hx : x ∈ c.C<GOAL>Urysohns.CU.approx n c x = 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>n : ℕ<VAR>x : X<VAR>hx : x ∉ c.U<GOAL>Urysohns.CU.approx n c x = 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>n : ℕ<VAR>x : X<GOAL>0 ≤ Urysohns.CU.approx n c x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>n : ℕ<VAR>x : X<GOAL>Urysohns.CU.approx n c x ≤ 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>BddAbove (Set.range fun n => Urysohns.CU.approx n c x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c₁ c₂ : Urysohns.CU P<VAR>h : c₁.U ⊆ c₂.C<VAR>n₁ n₂ : ℕ<VAR>x : X<GOAL>Urysohns.CU.approx n₂ c₂ x ≤ Urysohns.CU.approx n₁ c₁ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>n : ℕ<VAR>x : X<GOAL>Urysohns.CU.approx n c x ∈ Set.Icc (Urysohns.CU.approx n c.right x) (Urysohns.CU.approx n c.left x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>n : ℕ<VAR>x : X<GOAL>Urysohns.CU.approx n c x ≤ Urysohns.CU.approx (n + 1) c x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>Monotone fun n => Urysohns.CU.approx n c x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>Filter.Tendsto (fun n => Urysohns.CU.approx n c x) Filter.atTop (𝓝 (c.lim x))
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<VAR>h : x ∈ c.C<GOAL>c.lim x = 0
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<VAR>h : x ∉ c.U<GOAL>c.lim x = 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<VAR>n : ℕ<GOAL>Urysohns.CU.approx n c x ≤ c.lim x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>0 ≤ c.lim x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>c.lim x ≤ 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<VAR>x : X<GOAL>c.lim x ∈ Set.Icc 0 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>P : Set X → Prop<VAR>c : Urysohns.CU P<GOAL>Continuous c.lim
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, Set.EqOn (⇑f) 1 s ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>RegularSpace X<VAR>LocallyCompactSpace X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>h's : IsGδ s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, s = ⇑f ⁻¹' {1} ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1