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>s t : Set X<VAR>hf : IsLocalHomeomorphOn f t<VAR>hst : s ⊆ t<GOAL>IsLocalHomeomorphOn f 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>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>hgf : IsLocalHomeomorphOn (g ∘ f) s<VAR>hg : IsLocalHomeomorphOn g (f '' s)<VAR>cont : ∀ x ∈ s, ContinuousAt f x<GOAL>IsLocalHomeomorphOn f 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>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>hgf : IsLocalHomeomorphOn (g ∘ f) s<VAR>hf : IsLocalHomeomorphOn f s<GOAL>IsLocalHomeomorphOn g (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hf : IsLocalHomeomorphOn f s<VAR>x : X<VAR>hx : x ∈ s<GOAL>Filter.map f (𝓝 x) = 𝓝 (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hf : IsLocalHomeomorphOn f s<VAR>x : X<VAR>hx : x ∈ s<GOAL>ContinuousAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hf : IsLocalHomeomorphOn f s<GOAL>ContinuousOn f 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>g : Y → Z<VAR>f : X → Y<VAR>s : Set X<VAR>t : Set Y<VAR>hg : IsLocalHomeomorphOn g t<VAR>hf : IsLocalHomeomorphOn f s<VAR>h : Set.MapsTo f s t<GOAL>IsLocalHomeomorphOn (g ∘ f) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X ≃ₜ Y<GOAL>IsLocalHomeomorph ⇑f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsLocalHomeomorph f ↔ IsLocalHomeomorphOn f Set.univ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>hf : IsLocalHomeomorph f<GOAL>IsLocalHomeomorphOn f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<GOAL>IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, OpenEmbedding (U.restrict 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>IsLocalHomeomorph f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (x : X), ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source<GOAL>IsLocalHomeomorph f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>h : X ≃ₜ Y<GOAL>IsLocalHomeomorph ⇑h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph f<GOAL>IsLocallyInjective f
<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>g : Y → Z<VAR>f : X → Y<VAR>hgf : IsLocalHomeomorph (g ∘ f)<VAR>hg : IsLocalHomeomorph g<VAR>cont : Continuous f<GOAL>IsLocalHomeomorph f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph f<VAR>x : X<GOAL>Filter.map f (𝓝 x) = 𝓝 (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph f<GOAL>Continuous f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph f<GOAL>IsOpenMap f
<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>g : Y → Z<VAR>f : X → Y<VAR>hg : IsLocalHomeomorph g<VAR>hf : IsLocalHomeomorph f<GOAL>IsLocalHomeomorph (g ∘ f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph f<VAR>hi : Function.Injective f<GOAL>OpenEmbedding f
<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>g : Y → Z<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph g<VAR>hgf : OpenEmbedding (g ∘ f)<VAR>cont : Continuous f<GOAL>OpenEmbedding f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : IsLocalHomeomorph f<GOAL>TopologicalSpace.IsTopologicalBasis {U | ∃ V, IsOpen V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}
<VAR>x y : ℝ<VAR>hx : x ∈ unitInterval<VAR>hy : y ∈ unitInterval<GOAL>x * y ∈ unitInterval
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hxy : x ≤ y<GOAL>x / y ∈ unitInterval
<VAR>x : ℝ<GOAL>Int.fract x ∈ unitInterval
<VAR>t : ℝ<GOAL>t ∈ unitInterval ↔ 1 - t ∈ unitInterval
<VAR>x : ↑unitInterval<GOAL>↑x ≠ 0 ↔ x ≠ 0
<VAR>x : ↑unitInterval<GOAL>↑x ≠ 1 ↔ x ≠ 1
<VAR>x y : ↑unitInterval<GOAL>x * y ≤ x
<VAR>x y : ↑unitInterval<GOAL>x * y ≤ y
<VAR>x : ↑unitInterval<GOAL>unitInterval.symm (unitInterval.symm x) = x
<VAR>x : ↑unitInterval<GOAL>↑(unitInterval.symm x) = 1 - ↑x
<GOAL>∀ (a : ↑unitInterval), unitInterval.symmHomeomorph.symm a = unitInterval.symm a
<GOAL>∀ (a : ↑unitInterval), unitInterval.symmHomeomorph a = unitInterval.symm a
<VAR>t : ↑unitInterval<GOAL>1 / 2 ≤ ↑(unitInterval.symm t) ↔ ↑t ≤ 1 / 2
<VAR>x : ↑unitInterval<GOAL>0 ≤ ↑x
<VAR>x : ↑unitInterval<GOAL>0 ≤ 1 - ↑x
<VAR>x : ↑unitInterval<GOAL>↑x ≤ 1
<VAR>x : ↑unitInterval<GOAL>1 - ↑x ≤ 1
<VAR>t : ↑unitInterval<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>0 < x + ↑t
<VAR>t : ↑unitInterval<GOAL>0 ≤ t
<VAR>t : ↑unitInterval<GOAL>t ≤ 1
<VAR>a t : ℝ<VAR>ha : 0 < a<GOAL>a * t ∈ unitInterval ↔ t ∈ Set.Icc 0 (1 / a)
<VAR>t : ℝ<GOAL>2 * t - 1 ∈ unitInterval ↔ t ∈ Set.Icc (1 / 2) 1
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<GOAL>|↑(Set.projIcc a b h c) - ↑(Set.projIcc a b h d)| ≤ |c - d|
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : a ≤ b<VAR>δ : α<GOAL>↑(Set.Icc.addNSMul h δ 0) = a
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : a ≤ b<VAR>δ : α<VAR>Archimedean α<VAR>hδ : 0 < δ<GOAL>∃ m, ∀ n ≥ m, ↑(Set.Icc.addNSMul h δ n) = b
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : a ≤ b<VAR>δ : α<VAR>hδ : 0 ≤ δ<GOAL>Monotone (Set.Icc.addNSMul h δ)
<VAR>α : Type u_1<VAR>LinearOrderedAddCommGroup α<VAR>a b : α<VAR>h : a ≤ b<VAR>δ : α<VAR>hδ : 0 ≤ δ<VAR>t : ↑(Set.Icc a b)<VAR>n : ℕ<VAR>ht : t ∈ Set.Icc (Set.Icc.addNSMul h δ n) (Set.Icc.addNSMul h δ (n + 1))<GOAL>|↑t - ↑(Set.Icc.addNSMul h δ n)| ≤ δ
<VAR>ι : Sort u_1<VAR>a b : ℝ<VAR>h : a ≤ b<VAR>c : ι → Set ↑(Set.Icc a b)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : Set.univ ⊆ ⋃ i, c i<GOAL>∃ t, ↑(t 0) = a ∧ Monotone t ∧ (∃ m, ∀ n ≥ m, ↑(t n) = b) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set ↑unitInterval<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : Set.univ ⊆ ⋃ i, c i<GOAL>∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ c i
<VAR>ι : Sort u_1<VAR>c : ι → Set (↑unitInterval × ↑unitInterval)<VAR>hc₁ : ∀ (i : ι), IsOpen (c i)<VAR>hc₂ : Set.univ ⊆ ⋃ i, c i<GOAL>∃ t, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧ ∀ (n m : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ×ˢ Set.Icc (t m) (t (m + 1)) ⊆ c i
<VAR>x : ℝ<GOAL>Set.projIcc 0 1 ⋯ x = 0 ↔ x ≤ 0
<VAR>x : ℝ<GOAL>Set.projIcc 0 1 ⋯ x = 1 ↔ 1 ≤ x
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : 0 < a<GOAL>⇑(affineHomeomorph a b ⋯) '' Set.Icc 0 1 = Set.Icc b (a + b)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a < b<VAR>x : ↑(Set.Icc a b)<GOAL>↑((iccHomeoI a b h) x) = (↑x - a) / (b - a)
<VAR>𝕜 : Type u_1<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace 𝕜<VAR>TopologicalRing 𝕜<VAR>a b : 𝕜<VAR>h : a < b<VAR>x : ↑(Set.Icc 0 1)<GOAL>↑((iccHomeoI a b h).symm x) = (b - a) * ↑x + a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>r : Rel Y X<VAR>l : Filter Y<VAR>x : X<GOAL>Filter.RTendsto r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.core s ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>r : Rel Y X<VAR>l : Filter Y<VAR>x : X<GOAL>Filter.RTendsto' r l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : Y →. X<VAR>l : Filter Y<VAR>x : X<GOAL>Filter.PTendsto f l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f.core s ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>f : Y →. X<VAR>l : Filter Y<VAR>x : X<GOAL>Filter.PTendsto' f l (𝓝 x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f.preimage s ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X →. Y<VAR>h : PContinuous f<GOAL>IsOpen f.Dom
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X →. Y<GOAL>PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → Filter.PTendsto' f (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x : X<VAR>s : Set X<GOAL>ContinuousWithinAt f s x ↔ Filter.PTendsto (PFun.res f s) (𝓝 x) (𝓝 (f x))
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>ContinuousMap.compactOpen = TopologicalSpace.generateFrom (Set.image2 (fun K U => {f | Set.MapsTo (⇑f) K U}) {K | IsCompact K} {t | IsOpen t})
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>K : Set X<VAR>U : Set Y<VAR>hK : IsCompact K<VAR>hU : IsOpen U<GOAL>IsOpen {f | Set.MapsTo (⇑f) K U}
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>K : Set X<VAR>U : Set Y<VAR>f : C(X, Y)<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>h : Set.MapsTo (⇑f) K U<GOAL>∀ᶠ (g : C(X, Y)) in 𝓝 f, Set.MapsTo (⇑g) K U
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<GOAL>𝓝 f = ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen U), ⨅ (_ : Set.MapsTo (⇑f) K U), 𝓟 {g | Set.MapsTo (⇑g) K U}
<VAR>α : Type u_1<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>l : Filter α<VAR>f : α → C(Y, Z)<VAR>g : C(Y, Z)<GOAL>Filter.Tendsto f l (𝓝 g) ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → Set.MapsTo (⇑g) K U → ∀ᶠ (a : α) in l, Set.MapsTo (⇑(f a)) K U
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → C(Y, Z)<GOAL>Continuous f ↔ ∀ (K : Set Y), IsCompact K → ∀ (U : Set Z), IsOpen U → IsOpen {x | Set.MapsTo (⇑(f x)) K U}
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>g : C(Y, Z)<GOAL>Continuous g.comp
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>g : C(Y, Z)<VAR>hg : Inducing ⇑g<GOAL>Inducing g.comp
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>g : C(Y, Z)<VAR>hg : Embedding ⇑g<GOAL>Embedding g.comp
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X, Y)<GOAL>Continuous fun g => g.comp f
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<GOAL>Continuous fun x => x.2.comp x.1
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<VAR>α : Type u_6<VAR>l : Filter α<VAR>g : α → C(Y, Z)<VAR>g₀ : C(Y, Z)<VAR>f : α → C(X, Y)<VAR>f₀ : C(X, Y)<VAR>hg : Filter.Tendsto g l (𝓝 g₀)<VAR>hf : Filter.Tendsto f l (𝓝 f₀)<GOAL>Filter.Tendsto (fun a => (g a).comp (f a)) l (𝓝 (g₀.comp f₀))
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<VAR>X' : Type u_6<VAR>TopologicalSpace X'<VAR>a : X'<VAR>g : X' → C(Y, Z)<VAR>f : X' → C(X, Y)<VAR>hg : ContinuousAt g a<VAR>hf : ContinuousAt f a<GOAL>ContinuousAt (fun x => (g x).comp (f x)) a
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<VAR>X' : Type u_6<VAR>TopologicalSpace X'<VAR>a : X'<VAR>g : X' → C(Y, Z)<VAR>f : X' → C(X, Y)<VAR>s : Set X'<VAR>hg : ContinuousWithinAt g s a<VAR>hf : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => (g x).comp (f x)) s a
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<VAR>X' : Type u_6<VAR>TopologicalSpace X'<VAR>g : X' → C(Y, Z)<VAR>f : X' → C(X, Y)<VAR>s : Set X'<VAR>hg : ContinuousOn g s<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => (g x).comp (f x)) s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<VAR>X' : Type u_6<VAR>TopologicalSpace X'<VAR>g : X' → C(Y, Z)<VAR>f : X' → C(X, Y)<VAR>hg : Continuous g<VAR>hf : Continuous f<GOAL>Continuous fun x => (g x).comp (f x)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactPair Y Z<VAR>X' : Type u_6<VAR>TopologicalSpace X'<VAR>g : X' → C(Y, Z)<VAR>f : X' → C(X, Y)<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => (g x).comp (f x)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>LocallyCompactPair X Y<GOAL>Continuous fun p => p.1 p.2
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>a : X<GOAL>Continuous fun f => f a
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous DFunLike.coe
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>t : Set Y<VAR>ht : IsClosed t<VAR>s : Set X<GOAL>IsClosed {f | Set.MapsTo (⇑f) s t}
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>K : Set X<VAR>U : Set Y<VAR>hK : IsCompact K<VAR>hU : IsClopen U<GOAL>IsClopen {f | Set.MapsTo (⇑f) K U}
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g : C(X, Y)<GOAL>⇑f ⤳ ⇑g ↔ f ⤳ g
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f g : C(X, Y)<GOAL>Inseparable ⇑f ⇑g ↔ Inseparable f g
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<GOAL>Continuous fun F => ContinuousMap.restrict s F
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>s : Set X<GOAL>ContinuousMap.compactOpen ≤ TopologicalSpace.induced (ContinuousMap.restrict s) ContinuousMap.compactOpen
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>ContinuousMap.compactOpen = ⨅ K, ⨅ (_ : IsCompact K), TopologicalSpace.induced (ContinuousMap.restrict K) ContinuousMap.compactOpen
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : C(X, Y)<GOAL>𝓝 f = ⨅ s, ⨅ (_ : IsCompact s), Filter.comap (ContinuousMap.restrict s) (𝓝 (ContinuousMap.restrict s f))
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>F : ι → C(X, Y)<VAR>f : C(X, Y)<VAR>hFf : Filter.Tendsto F l (𝓝 f)<VAR>s : Set X<GOAL>Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (𝓝 (ContinuousMap.restrict s f))
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>F : ι → C(X, Y)<VAR>f : C(X, Y)<GOAL>Filter.Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Filter.Tendsto (fun i => ContinuousMap.restrict K (F i)) l (𝓝 (ContinuousMap.restrict K f))
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>WeaklyLocallyCompactSpace X<VAR>T2Space Y<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → C(X, Y)<GOAL>(∃ f, Filter.Tendsto F l (𝓝 f)) ↔ ∀ (s : Set X), IsCompact s → ∃ f, Filter.Tendsto (fun i => ContinuousMap.restrict s (F i)) l (𝓝 f)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>b : Y<GOAL>⇑(ContinuousMap.coev X Y b) = Prod.mk b
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>y : Y<VAR>s : Set X<GOAL>⇑(ContinuousMap.coev X Y y) '' s = {y} ×ˢ s
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous (ContinuousMap.coev X Y)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X × Y, Z)<VAR>a : X<VAR>b : Y<GOAL>(f.curry a) b = f (a, b)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : C(X × Y, Z)<GOAL>Continuous f.curry'
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>f : X → C(Y, Z)<VAR>h : Continuous (Function.uncurry fun x y => (f x) y)<GOAL>Continuous f
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactSpace (X × Y)<GOAL>Continuous ContinuousMap.curry
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactSpace Y<VAR>f : C(X, C(Y, Z))<GOAL>Continuous (Function.uncurry fun x y => (f x) y)
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactSpace Y<VAR>f : C(X, C(Y, Z))<GOAL>∀ (a : X × Y), f.uncurry a = Function.uncurry (fun x y => (f x) y) a
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactSpace X<VAR>LocallyCompactSpace Y<GOAL>Continuous ContinuousMap.uncurry
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>⇑ContinuousMap.const' = ContinuousMap.const X
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<GOAL>Continuous (ContinuousMap.const X)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Unique X<VAR>y : Y<VAR>x : X<GOAL>(Homeomorph.continuousMapOfUnique y) x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>Unique X<VAR>f : C(X, Y)<GOAL>Homeomorph.continuousMapOfUnique.symm f = f default
<VAR>X₀ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X₀<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactSpace Y<VAR>f : X₀ → X<VAR>hf : QuotientMap f<VAR>g : X × Y → Z<VAR>hg : Continuous fun p => g (f p.1, p.2)<GOAL>Continuous g
<VAR>X₀ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>TopologicalSpace X₀<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>LocallyCompactSpace Y<VAR>f : X₀ → X<VAR>hf : QuotientMap f<VAR>g : Y × X → Z<VAR>hg : Continuous fun p => g (p.1, f p.2)<GOAL>Continuous g
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>((𝓝 a).bind fun x => 𝓝[s] x) = 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∀ᶠ (y : α) in 𝓝 a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in 𝓝[s] a, p x) ↔ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>z : α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in 𝓝[s] z, p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>z : α<VAR>s : Set α<GOAL>z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[≠] z, x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[s] a = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, 𝓟 (t ∩ s)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<GOAL>𝓝[Set.univ] a = 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>p : β → Prop<VAR>s : β → Set α<VAR>a : α<VAR>h : (𝓝 a).HasBasis p s<VAR>t : Set α<GOAL>(𝓝[t] a).HasBasis p fun i => s i ∩ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>t : Set α<GOAL>(𝓝[t] a).HasBasis (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>t : Set α<VAR>a : α<VAR>s : Set α<GOAL>t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>t : Set α<VAR>a : α<VAR>s : Set α<GOAL>t ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝 x<VAR>t : Set α<GOAL>s \ t ∈ 𝓝[tᶜ] x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s t : Set α<VAR>hs : s ∈ 𝓝[t] x<VAR>t' : Set α<GOAL>s \ t' ∈ 𝓝[t \ t'] x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>a : α<VAR>h1 : s ∈ 𝓝 a<VAR>h2 : t ∈ 𝓝[s] a<GOAL>t ∈ 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>x : α<GOAL>t ∈ 𝓝[s] x ↔ ∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>x : α<GOAL>t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>x : α<GOAL>𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>x : α<GOAL>𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>t : Set α<VAR>a : α<VAR>h : a ∈ t<VAR>hs : s ∈ 𝓝 (π a)<GOAL>π ⁻¹' s ∈ 𝓝[t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 a<GOAL>s ∈ 𝓝[t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>∀ᶠ (x : α) in 𝓝[s] a, x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>t : Set α<VAR>a : α<VAR>h : t ∈ 𝓝 a<GOAL>s ∩ t ∈ 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>ha : a ∈ s<GOAL>pure a ≤ 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>ha : a ∈ s<VAR>ht : t ∈ 𝓝[s] a<GOAL>a ∈ t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>p : α → Prop<VAR>s : Set α<VAR>x : α<VAR>h : ∀ᶠ (y : α) in 𝓝[s] x, p y<VAR>hx : x ∈ s<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>l : Filter β<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<GOAL>Filter.Tendsto (fun x => a) l (𝓝[s] a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>t : Set α<VAR>h : t ∈ 𝓝[s] a<GOAL>𝓝[s] a = 𝓝[s ∩ t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>t : Set α<VAR>h : t ∈ 𝓝 a<GOAL>𝓝[s] a = 𝓝[s ∩ t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>t : Set α<VAR>h₀ : a ∈ t<VAR>h₁ : IsOpen t<GOAL>𝓝[s] a = 𝓝[s ∩ t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : s ∈ 𝓝[t] a<GOAL>𝓝[t] a ≤ 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[s] a ≤ 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t u : Set α<VAR>hs : s ∈ 𝓝 a<VAR>h₂ : t ∩ s = u ∩ s<GOAL>𝓝[t] a = 𝓝[u] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t u : Set α<VAR>h₀ : a ∈ s<VAR>h₁ : IsOpen s<VAR>h₂ : t ∩ s = u ∩ s<GOAL>𝓝[t] a = 𝓝[u] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<VAR>h : IsOpen s<VAR>ha : a ∈ s<GOAL>𝓝[s] a = 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>t : Set α<VAR>a : α<VAR>h : a ∈ t<VAR>ht : IsOpen t<VAR>hs : s ∈ 𝓝 (π a)<GOAL>π ⁻¹' s ∈ 𝓝 a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<GOAL>𝓝[∅] a = ⊥
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<GOAL>𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_5<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set α<VAR>a : α<GOAL>𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>S : Set (Set α)<VAR>hS : S.Finite<VAR>a : α<GOAL>𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a