ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : SpecializingMap f<VAR>s : Set X<VAR>hs : StableUnderSpecialization s<GOAL>StableUnderSpecialization (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure {x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>SpecializingMap f ↔ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>SpecializingMap f ↔ ∀ (x : X), f '' closure {x} = closure {f x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>SpecializingMap f ↔ ∀ (x : X), IsClosed (f '' closure {x})
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsClosedMap f<GOAL>SpecializingMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>h : StableUnderSpecialization (Set.range f)<GOAL>SpecializingMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<VAR>h : StableUnderGeneralization (Set.range f)<GOAL>GeneralizingMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : OpenEmbedding f<GOAL>GeneralizingMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : SpecializingMap f<GOAL>StableUnderSpecialization (Set.range f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : GeneralizingMap f<VAR>s : Set X<VAR>hs : StableUnderGeneralization s<GOAL>StableUnderGeneralization (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>GeneralizingMap f ↔ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : GeneralizingMap f<GOAL>StableUnderGeneralization (Set.range f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>(x ~ᵢ y) ↔ 𝓝 x = 𝓝 y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>(x ~ᵢ y) ↔ x ⤳ y ∧ y ⤳ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ~ᵢ y<GOAL>x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ~ᵢ y<GOAL>y ⤳ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h₁ : x ⤳ y<VAR>h₂ : y ⤳ x<GOAL>x ~ᵢ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>(x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen s → (x ∈ s ↔ y ∈ s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>¬(x ~ᵢ y) ↔ ∃ s, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>(x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed s → (x ∈ s ↔ y ∈ s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>(x ~ᵢ y) ↔ x ∈ closure {y} ∧ y ∈ closure {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>(x ~ᵢ y) ↔ closure {x} = closure {y}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>h : 𝓝[s] x = 𝓝[s] y<GOAL>x ~ᵢ y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>(f x ~ᵢ f y) ↔ (x ~ᵢ y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>p : X → Prop<VAR>x y : Subtype p<GOAL>(x ~ᵢ y) ↔ (↑x ~ᵢ ↑y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₁ x₂ : X<VAR>y₁ y₂ : Y<GOAL>((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x₁ x₂ : X<VAR>y₁ y₂ : Y<VAR>hx : x₁ ~ᵢ x₂<VAR>hy : y₁ ~ᵢ y₂<GOAL>(x₁, y₁) ~ᵢ (x₂, y₂)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>f g : (i : ι) → π i<GOAL>(f ~ᵢ g) ↔ ∀ (i : ι), f i ~ᵢ g i
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>x ~ᵢ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>e : x = y<GOAL>x ~ᵢ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ~ᵢ y<GOAL>y ~ᵢ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y z : X<VAR>h₁ : x ~ᵢ y<VAR>h₂ : y ~ᵢ z<GOAL>x ~ᵢ z
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>h : x ~ᵢ y<GOAL>𝓝 x = 𝓝 y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>h : x ~ᵢ y<VAR>hs : IsOpen s<GOAL>x ∈ s ↔ y ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>h : x ~ᵢ y<VAR>hs : IsClosed s<GOAL>x ∈ s ↔ y ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>f : X → Y<VAR>h : x ~ᵢ y<VAR>hx : ContinuousAt f x<VAR>hy : ContinuousAt f y<GOAL>f x ~ᵢ f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x y : X<VAR>f : X → Y<VAR>h : x ~ᵢ y<VAR>hf : Continuous f<GOAL>f x ~ᵢ f y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hx : x ∈ s<VAR>hy : y ∉ s<GOAL>¬(x ~ᵢ y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>hx : x ∈ s<VAR>hy : y ∉ s<GOAL>¬(x ~ᵢ y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>QuotientMap SeparationQuotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Continuous SeparationQuotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>SeparationQuotient.mk x = SeparationQuotient.mk y ↔ (x ~ᵢ y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Function.Surjective SeparationQuotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Set.range SeparationQuotient.mk = Set.univ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsOpenMap SeparationQuotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Inducing SeparationQuotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>IsClosedMap SeparationQuotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>Filter.comap SeparationQuotient.mk (𝓝 (SeparationQuotient.mk x)) = 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>Filter.comap SeparationQuotient.mk (𝓝ˢ (SeparationQuotient.mk '' s)) = 𝓝ˢ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<GOAL>Filter.map SeparationQuotient.mk (𝓝 x) = 𝓝 (SeparationQuotient.mk x)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>Filter.map SeparationQuotient.mk (𝓝ˢ s) = 𝓝ˢ (SeparationQuotient.mk '' s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t : Set (SeparationQuotient X)<GOAL>Filter.comap SeparationQuotient.mk (𝓝ˢ t) = 𝓝ˢ (SeparationQuotient.mk ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t : Set (SeparationQuotient X)<GOAL>SeparationQuotient.mk ⁻¹' closure t = closure (SeparationQuotient.mk ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t : Set (SeparationQuotient X)<GOAL>SeparationQuotient.mk ⁻¹' interior t = interior (SeparationQuotient.mk ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>t : Set (SeparationQuotient X)<GOAL>SeparationQuotient.mk ⁻¹' frontier t = frontier (SeparationQuotient.mk ⁻¹' t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<GOAL>SeparationQuotient.mk '' closure s = closure (SeparationQuotient.mk '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>y : Y<GOAL>Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓝 (x, y)) = 𝓝 (SeparationQuotient.mk x, SeparationQuotient.mk y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set (SeparationQuotient X)<VAR>x : X<GOAL>Filter.map SeparationQuotient.mk (𝓝[SeparationQuotient.mk ⁻¹' s] x) = 𝓝[s] SeparationQuotient.mk x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>QuotientMap (Prod.map SeparationQuotient.mk SeparationQuotient.mk)
<VAR>X : Type u_1<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>f : X → α<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>x : X<GOAL>SeparationQuotient.lift f hf (SeparationQuotient.mk x) = f x
<VAR>X : Type u_1<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>f : X → α<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<GOAL>SeparationQuotient.lift f hf ∘ SeparationQuotient.mk = f
<VAR>X : Type u_1<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>x : X<VAR>f : X → α<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>l : Filter α<GOAL>Filter.Tendsto (SeparationQuotient.lift f hf) (𝓝 (SeparationQuotient.mk x)) l ↔ Filter.Tendsto f (𝓝 x) l
<VAR>X : Type u_1<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>x : X<VAR>f : X → α<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>s : Set (SeparationQuotient X)<VAR>l : Filter α<GOAL>Filter.Tendsto (SeparationQuotient.lift f hf) (𝓝[s] SeparationQuotient.mk x) l ↔ Filter.Tendsto f (𝓝[SeparationQuotient.mk ⁻¹' s] x) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>f : X → Y<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<GOAL>ContinuousAt (SeparationQuotient.lift f hf) (SeparationQuotient.mk x) ↔ ContinuousAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>x : X<VAR>f : X → Y<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>s : Set (SeparationQuotient X)<GOAL>ContinuousWithinAt (SeparationQuotient.lift f hf) s (SeparationQuotient.mk x) ↔ ContinuousWithinAt f (SeparationQuotient.mk ⁻¹' s) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>s : Set (SeparationQuotient X)<GOAL>ContinuousOn (SeparationQuotient.lift f hf) s ↔ ContinuousOn f (SeparationQuotient.mk ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<GOAL>Continuous (SeparationQuotient.lift f hf) ↔ Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<GOAL>SeparationQuotient.lift₂ f hf (SeparationQuotient.mk x) (SeparationQuotient.mk y) = f x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<VAR>l : Filter α<GOAL>Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf)) (𝓝 (SeparationQuotient.mk x, SeparationQuotient.mk y)) l ↔ Filter.Tendsto (Function.uncurry f) (𝓝 (x, y)) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>α : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y → α<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>l : Filter α<GOAL>Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf)) (𝓝[s] (SeparationQuotient.mk x, SeparationQuotient.mk y)) l ↔ Filter.Tendsto (Function.uncurry f) (𝓝[Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s] (x, y)) l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>x : X<VAR>y : Y<GOAL>ContinuousAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔ ContinuousAt (Function.uncurry f) (x, y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>x : X<VAR>y : Y<GOAL>ContinuousWithinAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) s (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔ ContinuousWithinAt (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s) (x, y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<GOAL>ContinuousOn (Function.uncurry (SeparationQuotient.lift₂ f hf)) s ↔ ContinuousOn (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<GOAL>Continuous (Function.uncurry (SeparationQuotient.lift₂ f hf)) ↔ Continuous (Function.uncurry f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g : X → Y<VAR>h : ∀ (x : X), f x ~ᵢ g x<GOAL>Continuous f ↔ Continuous g
<VAR>X : TopCat<VAR>F : TopCat.Presheaf (Type v) X<VAR>x : ↑X<GOAL>Function.Surjective (F.stalkToFiber x)
<VAR>X : TopCat<VAR>F : TopCat.Presheaf (Type v) X<VAR>x : ↑X<GOAL>Function.Injective (F.stalkToFiber x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>hind : X.str = ⊤<VAR>F : TopCat.Presheaf C X<VAR>it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))<GOAL>F.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : TopCat<VAR>hind : X.str = ⊤<VAR>F : TopCat.Presheaf C X<GOAL>F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : TopCat.Presheaf C (TopCat.of PUnit.{u_1 + 1})<VAR>it : CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥))<GOAL>F.IsSheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : TopCat.Presheaf C (TopCat.of PUnit.{u_1 + 1})<GOAL>F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X : TopCat<VAR>ℱ 𝒢 : TopCat.Presheaf C X<VAR>T : ℱ ⟶ 𝒢<GOAL>TopCat.Presheaf.IsLocallySurjective T ↔ ∀ (U : TopologicalSpace.Opens ↑X) (t : (CategoryTheory.forget C).obj (𝒢.obj (Opposite.op U))), ∀ x ∈ U, ∃ V ι, (∃ s, (T.app (Opposite.op V)) s = TopCat.Presheaf.restrict t ι) ∧ x ∈ V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X : TopCat<VAR>ℱ 𝒢 : TopCat.Presheaf C X<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)<VAR>T : ℱ ⟶ 𝒢<GOAL>TopCat.Presheaf.IsLocallySurjective T ↔ ∀ (x : ↑X), Function.Surjective ⇑((TopCat.Presheaf.stalkFunctor C x).map T)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<GOAL>EMetric.infEdist x ∅ = ⊤
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<VAR>d : ℝ≥0∞<GOAL>d ≤ EMetric.infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s t : Set α<GOAL>EMetric.infEdist x (s ∪ t) = EMetric.infEdist x s ⊓ EMetric.infEdist x t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : ι → Set α<VAR>x : α<GOAL>EMetric.infEdist x (⋃ i, f i) = ⨅ i, EMetric.infEdist x (f i)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>ι : Type u_2<VAR>f : ι → Set α<VAR>I : Set ι<VAR>x : α<GOAL>EMetric.infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, EMetric.infEdist x (f i)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>EMetric.infEdist x {y} = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s : Set α<VAR>h : y ∈ s<GOAL>EMetric.infEdist x s ≤ edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<VAR>h : x ∈ s<GOAL>EMetric.infEdist x s = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>EMetric.infEdist x t ≤ EMetric.infEdist x s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<VAR>r : ℝ≥0∞<GOAL>EMetric.infEdist x s < r ↔ ∃ y ∈ s, edist x y < r
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s : Set α<GOAL>EMetric.infEdist x s ≤ EMetric.infEdist y s + edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s : Set α<GOAL>EMetric.infEdist x s ≤ edist x y + EMetric.infEdist y s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>s : Set α<VAR>hy : y ∈ s<GOAL>edist x y ≤ EMetric.infEdist x s + EMetric.diam s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>Continuous fun x => EMetric.infEdist x s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>EMetric.infEdist x (closure s) = EMetric.infEdist x s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>x ∈ closure s ↔ EMetric.infEdist x s = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<VAR>h : IsClosed s<GOAL>x ∈ s ↔ EMetric.infEdist x s = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>E : Set α<GOAL>0 < EMetric.infEdist x E ↔ x ∉ closure E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>E : Set α<GOAL>0 < EMetric.infEdist x (closure E) ↔ x ∉ closure E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>E : Set α<VAR>h : x ∉ closure E<GOAL>∃ ε, 0 < ε ∧ ENNReal.ofReal ε < EMetric.infEdist x E
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<VAR>r : ℝ≥0∞<VAR>h : r < EMetric.infEdist x s<GOAL>Disjoint (EMetric.closedBall x r) s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>x : α<VAR>t : Set α<VAR>Φ : α → β<VAR>hΦ : Isometry Φ<GOAL>EMetric.infEdist (Φ x) (Φ '' t) = EMetric.infEdist x t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>M : Type u_2<VAR>VAdd M α<VAR>IsometricVAdd M α<VAR>c : M<VAR>x : α<VAR>s : Set α<GOAL>EMetric.infEdist (c +ᵥ x) (c +ᵥ s) = EMetric.infEdist x s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>M : Type u_2<VAR>SMul M α<VAR>IsometricSMul M α<VAR>c : M<VAR>x : α<VAR>s : Set α<GOAL>EMetric.infEdist (c • x) (c • s) = EMetric.infEdist x s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>U : Set α<VAR>hU : IsOpen U<GOAL>∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>hne : s.Nonempty<VAR>x : α<GOAL>∃ y ∈ s, EMetric.infEdist x s = edist x y
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<GOAL>∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
<VAR>α : Type u_2<VAR>PseudoEMetricSpace α<VAR>s t : Set α<GOAL>EMetric.hausdorffEdist s t = (⨆ x ∈ s, EMetric.infEdist x t) ⊔ ⨆ y ∈ t, EMetric.infEdist y s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>EMetric.hausdorffEdist s s = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<GOAL>EMetric.hausdorffEdist s t = EMetric.hausdorffEdist t s
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, EMetric.infEdist x t ≤ r<VAR>H2 : ∀ x ∈ t, EMetric.infEdist x s ≤ r<GOAL>EMetric.hausdorffEdist s t ≤ r
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r<VAR>H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r<GOAL>EMetric.hausdorffEdist s t ≤ r
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>h : x ∈ s<GOAL>EMetric.infEdist x t ≤ EMetric.hausdorffEdist s t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r : ℝ≥0∞<VAR>h : x ∈ s<VAR>H : EMetric.hausdorffEdist s t < r<GOAL>∃ y ∈ t, edist x y < r
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s t : Set α<GOAL>EMetric.infEdist x t ≤ EMetric.infEdist x s + EMetric.hausdorffEdist s t
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>s t : Set α<VAR>Φ : α → β<VAR>h : Isometry Φ<GOAL>EMetric.hausdorffEdist (Φ '' s) (Φ '' t) = EMetric.hausdorffEdist s t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>EMetric.hausdorffEdist s t ≤ EMetric.diam (s ∪ t)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t u : Set α<GOAL>EMetric.hausdorffEdist s u ≤ EMetric.hausdorffEdist s t + EMetric.hausdorffEdist t u
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<GOAL>EMetric.hausdorffEdist s t = 0 ↔ closure s = closure t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>EMetric.hausdorffEdist s (closure s) = 0
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<GOAL>EMetric.hausdorffEdist (closure s) t = EMetric.hausdorffEdist s t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<GOAL>EMetric.hausdorffEdist s (closure t) = EMetric.hausdorffEdist s t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<GOAL>EMetric.hausdorffEdist (closure s) (closure t) = EMetric.hausdorffEdist s t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>EMetric.hausdorffEdist s t = 0 ↔ s = t
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<VAR>ne : s.Nonempty<GOAL>EMetric.hausdorffEdist s ∅ = ⊤
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>hs : s.Nonempty<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>t.Nonempty
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s t : Set α<VAR>fin : EMetric.hausdorffEdist s t ≠ ⊤<GOAL>s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>Metric.infDist x s = ⨅ y, dist x ↑y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>0 ≤ Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>Metric.infDist x ∅ = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>h : s.Nonempty<GOAL>EMetric.infEdist x s ≠ ⊤
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>EMetric.infEdist x s = ⊤ ↔ s = ∅
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>h : x ∈ s<GOAL>Metric.infDist x s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x y : α<GOAL>Metric.infDist x {y} = dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>h : y ∈ s<GOAL>Metric.infDist x s ≤ dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s t : Set α<VAR>x : α<VAR>h : s ⊆ t<VAR>hs : s.Nonempty<GOAL>Metric.infDist x t ≤ Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>r : ℝ<VAR>hs : s.Nonempty<GOAL>Metric.infDist x s < r ↔ ∃ y ∈ s, dist x y < r
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<GOAL>Metric.infDist x s ≤ Metric.infDist y s + dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>h : dist x y < Metric.infDist x s<GOAL>y ∉ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>Disjoint (Metric.ball x (Metric.infDist x s)) s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>Metric.ball x (Metric.infDist x s) ⊆ sᶜ
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>Metric.ball x (Metric.infDist x sᶜ) ⊆ s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>r : ℝ<VAR>h : r < Metric.infDist x s<GOAL>Disjoint (Metric.closedBall x r) s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x y : α<VAR>hs : Bornology.IsBounded s<VAR>hy : y ∈ s<GOAL>dist x y ≤ Metric.infDist x s + Metric.diam s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>LipschitzWith 1 fun x => Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>UniformContinuous fun x => Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>Continuous fun x => Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<GOAL>Metric.infDist x (closure s) = Metric.infDist x s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ closure s<GOAL>Metric.infDist x s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>h : s.Nonempty<GOAL>x ∈ closure s ↔ Metric.infDist x s = 0
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>x : α<VAR>h : IsClosed s<VAR>hs : s.Nonempty<GOAL>x ∈ s ↔ Metric.infDist x s = 0