ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>One X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Continuous f<GOAL>IsOpen (Function.mulSupport f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>Zero X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Continuous f<GOAL>IsOpen (Function.support f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>𝓝[{y}ᶜ] x = 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>h : x ≠ y<VAR>s : Set X<GOAL>𝓝[s \ {y}] x = 𝓝[s] x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<GOAL>𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>p : X → Prop<GOAL>IsOpen {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>b : Set (Set X)<VAR>hb : TopologicalSpace.IsTopologicalBasis b<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ a ∈ b, x ∈ a ∧ y ∉ a
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Finset X<GOAL>IsClosed ↑s
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>[T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of, ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T1Space X ↔ Continuous ⇑CofiniteTopology.of
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<GOAL>Continuous ⇑CofiniteTopology.of
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T1Space X ↔ Pairwise fun x y => ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>Disjoint (pure x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>Disjoint (𝓝 x) (pure y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>h : x ⤳ y<GOAL>x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<GOAL>x ⤳ y ↔ x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<GOAL>(fun x x_1 => x ⤳ x_1) = Eq
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>a b : X<GOAL>pure a ≤ 𝓝 b ↔ a = b
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>a b : X<GOAL>𝓝 a ≤ 𝓝 b ↔ a = b
<VAR>X : Type u_1<GOAL>Antitone (@T1Space X)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>DecidableEq X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x x' : X<VAR>y : Y<VAR>hne : x' ≠ x<GOAL>ContinuousWithinAt (Function.update f x y) s x' ↔ ContinuousWithinAt f s x'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>DecidableEq X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>x x' : X<VAR>y : Y<VAR>hne : x' ≠ x<GOAL>ContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>DecidableEq X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<GOAL>ContinuousOn (Function.update f x y) s ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Filter.Tendsto f (𝓝[s \ {x}] x) (𝓝 y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>f : X → Y<VAR>hf : Function.Injective f<VAR>hf' : Continuous f<VAR>T1Space Y<GOAL>T1Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T1Space Y<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>T1Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<GOAL>{x}ᶜ ∈ 𝓝 y ↔ y ≠ x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>h : y ≠ x<GOAL>{x}ᶜ ∈ 𝓝 y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<GOAL>closure {x} = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Set X<VAR>hs : s.Subsingleton<GOAL>(closure s).Subsingleton
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Set X<GOAL>(closure s).Subsingleton ↔ s.Subsingleton
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T1Space Y<VAR>y : Y<GOAL>IsClosedMap (Function.const X y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>s : Set X<VAR>hxy : x ≠ y<GOAL>𝓝[insert y s] x = 𝓝[s] x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x y : X<VAR>s t : Set X<VAR>hu : t ⊆ insert y s<GOAL>insert x s ∈ 𝓝[t] x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<GOAL>(𝓝 x).ker = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>s : ι → Set X<VAR>x : X<VAR>h : (𝓝 x).HasBasis p s<GOAL>⋂ i, ⋂ (_ : p i), s i = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<VAR>s : Set X<GOAL>{x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s t : Set X<GOAL>𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s t : Set X<GOAL>𝓝ˢ s = 𝓝ˢ t ↔ s = t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<GOAL>Function.Injective 𝓝ˢ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<GOAL>StrictMono 𝓝ˢ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Set X<VAR>x : X<GOAL>𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Set X<VAR>hs : Dense s<VAR>x : X<VAR>(𝓝[≠] x).NeBot<GOAL>Dense (s \ {x})
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>∀ (x : X), (𝓝[≠] x).NeBot<VAR>s : Set X<VAR>hs : Dense s<VAR>t : Finset X<GOAL>Dense (s \ ↑t)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>∀ (x : X), (𝓝[≠] x).NeBot<VAR>s : Set X<VAR>hs : Dense s<VAR>t : Set X<VAR>ht : t.Finite<GOAL>Dense (s \ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T1Space Y<VAR>f : X → Y<VAR>x : X<VAR>y : Y<VAR>h : Filter.Tendsto f (𝓝 x) (𝓝 y)<GOAL>f x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace Y<VAR>T1Space Y<VAR>g : X → Y<VAR>l : Filter X<VAR>b₁ b₂ : Y<VAR>hg : Filter.Tendsto g l (𝓝 b₁)<VAR>hb : b₁ ≠ b₂<GOAL>∀ᶠ (z : X) in l, g z ≠ b₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T1Space Y<VAR>g : X → Y<VAR>x : X<VAR>y : Y<VAR>hg1 : ContinuousAt g x<VAR>hg2 : g x ≠ y<GOAL>∀ᶠ (z : X) in 𝓝 x, g z ≠ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>a b : X<VAR>h : a ≠ b<GOAL>∀ᶠ (x : X) in 𝓝 a, x ≠ b
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>a b : X<VAR>s : Set X<VAR>h : a ≠ b<GOAL>∀ᶠ (x : X) in 𝓝[s] a, x ≠ b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T1Space Y<VAR>f : X → Y<VAR>x : X<VAR>y : Y<VAR>h : Filter.Tendsto f (𝓝 x) (𝓝 y)<GOAL>ContinuousAt f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>l : Filter Y<VAR>l.NeBot<VAR>c d : X<GOAL>Filter.Tendsto (fun x => c) l (𝓝 d) ↔ c = d
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<VAR>hsf : s.Finite<GOAL>IsOpen {x}
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>T1Space X<VAR>x : X<VAR>hx : (𝓝[≠] x).NeBot<VAR>s : Set X<VAR>hs : s ∈ 𝓝 x<GOAL>s.Infinite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T1Space X<VAR>TopologicalSpace Y<VAR>s : Set X<VAR>hs : s.Finite<VAR>f : X → Y<GOAL>ContinuousOn f s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>PreconnectedSpace X<VAR>DiscreteTopology X<GOAL>Subsingleton X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Set X<VAR>h : IsPreconnected s<VAR>hs : s.Nontrivial<GOAL>s.Infinite
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ConnectedSpace X<VAR>Nontrivial X<VAR>T1Space X<GOAL>Infinite X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x : X<VAR>T1Space X<GOAL>IsGδ {x}ᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>T1Space X<VAR>hs : s.Countable<GOAL>IsGδ sᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>T1Space X<VAR>hs : s.Finite<GOAL>IsGδ sᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>T1Space X<VAR>hs : s.Subsingleton<GOAL>IsGδ sᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>s : Finset X<GOAL>IsGδ (↑s)ᶜ
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>T1Space X<VAR>x : X<GOAL>IsGδ {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>s : Set X<VAR>T1Space X<VAR>hs : s.Finite<GOAL>IsGδ s
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T1Space (SeparationQuotient X) ↔ R0Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>A : Set X<VAR>h : A.Subsingleton<GOAL>IsClosed A
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>A : Set X<VAR>a : X<GOAL>IsClosed (A ∩ {a})
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T1Space X<VAR>A : Set X<VAR>a : X<GOAL>IsClosed ({a} ∩ A)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>{x} ∈ 𝓝[s] x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>𝓝[s] x = pure x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>p : ι → Prop<VAR>t : ι → Set X<VAR>s : Set X<VAR>DiscreteTopology ↑s<VAR>x : X<VAR>hb : (𝓝 x).HasBasis p t<VAR>hx : x ∈ s<GOAL>∃ i, p i ∧ t i ∩ s = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ U ∈ 𝓝 x, U ∩ s = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ U, IsOpen U ∧ U ∩ s = {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>s : Set X<VAR>DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ U ∈ 𝓝[≠] x, Disjoint U s
<VAR>ι : Type u_3<VAR>β : ι → Type u_4<VAR>DecidableEq ι<VAR>(i : ι) → TopologicalSpace (β i)<VAR>x : (i : ι) → β i<VAR>i : ι<VAR>∀ (i : ι), T1Space (β i)<GOAL>ClosedEmbedding (Function.update x i)
<VAR>X : Type u_3<VAR>TopologicalSpace X<VAR>self : R1Space X<VAR>x y : X<GOAL>x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_3<VAR>TopologicalSpace X<GOAL>R1Space X ↔ ∀ (x y : X), x ⤳ y ∨ Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>x y : X<GOAL>Disjoint (𝓝 x) (𝓝 y) ↔ ¬x ⤳ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>x y : X<GOAL>x ⤳ y ↔ ¬Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>x y : X<GOAL>Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y
<VAR>X : Type u_3<VAR>TopologicalSpace X<GOAL>R1Space X ↔ ∀ (x y : X), Inseparable x y ∨ Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<GOAL>IsClosed {p | p.1 ⤳ p.2}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<GOAL>IsClosed {p | Inseparable p.1 p.2}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>y : X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>closure K = ⋃ x ∈ K, {y | Inseparable x y}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>closure K = ⋃ x ∈ K, closure {x}
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>U : Set X<VAR>hU : IsOpen U<VAR>hKU : K ⊆ U<GOAL>closure K ⊆ U
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>IsCompact (closure K)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>s K : Set X<VAR>hK : IsCompact K<VAR>h : s ⊆ K<GOAL>IsCompact (closure s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>s : Set X<GOAL>(∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>K L : Set X<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>h'L : IsClosed L<VAR>hd : Disjoint K L<GOAL>SeparatedNhds K L
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>K U V : Set X<VAR>hK : IsCompact K<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>h2K : K ⊆ U ∪ V<GOAL>∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>s : Set X<VAR>hs : IsCompact s<VAR>ι : Type u_3<VAR>t : Finset ι<VAR>U : ι → Set X<VAR>hU : ∀ i ∈ t, IsOpen (U i)<VAR>hsC : s ⊆ ⋃ i ∈ t, U i<GOAL>∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>hc : Continuous f<VAR>hspec : ∀ (x y : Y), f x ⤳ f y → x ⤳ y<GOAL>R1Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R1Space X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<GOAL>R1Space Y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>R1Space X<VAR>f : Y → X<GOAL>R1Space Y
<VAR>X : Type u_3<VAR>T : Set (TopologicalSpace X)<VAR>hT : ∀ t ∈ T, R1Space X<GOAL>R1Space X
<VAR>ι : Type u_3<VAR>X : Type u_4<VAR>t : ι → TopologicalSpace X<VAR>ht : ∀ (i : ι), R1Space X<GOAL>R1Space X
<VAR>X : Type u_3<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : R1Space X<VAR>h₂ : R1Space X<GOAL>R1Space X
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>R1Space Y<VAR>f : X → Y<VAR>x : X<VAR>K : Set X<VAR>s : Set Y<VAR>hf : Continuous f<VAR>hs : s ∈ 𝓝 (f x)<VAR>hKc : IsCompact K<VAR>hKx : K ∈ 𝓝 x<GOAL>∃ K ∈ 𝓝 x, IsCompact K ∧ Set.MapsTo f K s
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>x : X<VAR>L : Set X<VAR>hLc : IsCompact L<VAR>hxL : L ∈ 𝓝 x<GOAL>(𝓝 x).HasBasis (fun K => K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) fun x => x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<GOAL>Filter.coclosedCompact X = Filter.cocompact X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<GOAL>Bornology.relativelyCompact X = Bornology.inCompact X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>WeaklyLocallyCompactSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun K => K ∈ 𝓝 x ∧ IsCompact K ∧ IsClosed K) fun x => x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>WeaklyLocallyCompactSpace X<VAR>x : X<GOAL>∃ K ∈ 𝓝 x, IsCompact K ∧ IsClosed K
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>WeaklyLocallyCompactSpace X<VAR>K : Set X<VAR>hK : IsCompact K<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<VAR>WeaklyLocallyCompactSpace X<VAR>x : X<GOAL>∃ U, IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)
<VAR>X : Type u<VAR>TopologicalSpace X<GOAL>T2Space X ↔ Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>self : T2Space X<GOAL>Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T2Space X ↔ Pairwise fun x y => Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x y : X<GOAL>Disjoint (𝓝 x) (𝓝 y) ↔ x ≠ y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<GOAL>Pairwise (Disjoint on 𝓝)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s : Set X<GOAL>s.PairwiseDisjoint 𝓝
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>∃ U, (∀ (x : X), x ∈ U x ∧ IsOpen (U x)) ∧ s.PairwiseDisjoint U
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T2Space (SeparationQuotient X) ↔ R1Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>R1Space X<GOAL>T2Space X ↔ T0Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T2Space X ↔ ∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x y : X<VAR>h : (𝓝 x ⊓ 𝓝 y).NeBot<GOAL>x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T2Space X ↔ Pairwise fun x y => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ Disjoint u v
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>T2Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>T2Space X ↔ IsClosed (Set.diagonal X)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<GOAL>IsClosed (Set.diagonal X)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f : Y → X<VAR>l : Filter Y<VAR>a b : X<VAR>l.NeBot<VAR>ha : Filter.Tendsto f l (𝓝 a)<VAR>hb : Filter.Tendsto f l (𝓝 b)<GOAL>a = b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f : Y → X<VAR>l : Filter Y<VAR>a b : X<GOAL>l.NeBot → Filter.Tendsto f l (𝓝 a) → Filter.Tendsto f l (𝓝 b) → a = b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f g : Y → X<VAR>l : Filter Y<VAR>a b : X<VAR>l.NeBot<VAR>ha : Filter.Tendsto f l (𝓝 a)<VAR>hb : Filter.Tendsto g l (𝓝 b)<VAR>hfg : f =ᶠ[l] g<GOAL>a = b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f g : Y → X<VAR>l : Filter Y<VAR>a b : X<VAR>ha : Filter.Tendsto f l (𝓝 a)<VAR>hb : Filter.Tendsto g l (𝓝 b)<VAR>hfg : ∃ᶠ (x : Y) in l, f x = g x<GOAL>a = b
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>s : Set X<VAR>inj : Set.InjOn f s<VAR>sc : IsCompact s<VAR>fc : ∀ x ∈ s, ContinuousAt f x<VAR>loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, Set.InjOn f u<GOAL>∃ t ∈ 𝓝ˢ s, Set.InjOn f t
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>s : Set X<VAR>inj : Set.InjOn f s<VAR>sc : IsCompact s<VAR>fc : ∀ x ∈ s, ContinuousAt f x<VAR>loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, Set.InjOn f u<GOAL>∃ t, IsOpen t ∧ s ⊆ t ∧ Set.InjOn f t
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f : Filter X<VAR>x : X<VAR>f.NeBot<VAR>h : f ≤ 𝓝 x<GOAL>lim f = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f : Filter X<VAR>f.NeBot<VAR>h : ∃ x, f ≤ 𝓝 x<VAR>x : X<GOAL>lim f = x ↔ f ≤ 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>x : X<VAR>F : Ultrafilter X<GOAL>F.lim = x ↔ ↑F ≤ 𝓝 x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>CompactSpace X<VAR>U : Set X<GOAL>IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x : X<VAR>f : Filter Y<VAR>f.NeBot<VAR>g : Y → X<VAR>h : Filter.Tendsto g f (𝓝 x)<GOAL>limUnder f g = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>f : Filter Y<VAR>f.NeBot<VAR>g : Y → X<VAR>h : ∃ x, Filter.Tendsto g f (𝓝 x)<VAR>x : X<GOAL>limUnder f g = x ↔ Filter.Tendsto g f (𝓝 x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>T2Space X<VAR>TopologicalSpace Y<VAR>f : Y → X<VAR>h : Continuous f<VAR>y : Y<GOAL>limUnder (𝓝 y) f = f y
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x : X<GOAL>lim (𝓝 x) = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x : X<GOAL>limUnder (𝓝 x) id = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x : X<VAR>s : Set X<VAR>h : x ∈ closure s<GOAL>lim (𝓝[s] x) = x
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>T2Space X<VAR>x : X<VAR>s : Set X<VAR>h : x ∈ closure s<GOAL>limUnder (𝓝[s] x) id = x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>x y : X<VAR>h : f x ≠ f y<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>f : X → Y<VAR>hf : OpenEmbedding f<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ u v, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hinj : Function.Injective f<VAR>hc : Continuous f<GOAL>T2Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>T2Space X
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>x y : X<GOAL>t2Quotient.mk x = t2Quotient.mk y ↔ ∀ (s : Setoid X), T2Space (Quotient s) → s.Rel x y
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Function.Surjective t2Quotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<GOAL>Continuous t2Quotient.mk
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>motive : t2Quotient X → Prop<VAR>q : t2Quotient X<VAR>h : ∀ (x : X), motive (t2Quotient.mk x)<GOAL>motive q
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>motive : t2Quotient X → t2Quotient Y → Prop<VAR>q : t2Quotient X<VAR>q' : t2Quotient Y<VAR>h : ∀ (x : X) (y : Y), motive (t2Quotient.mk x) (t2Quotient.mk y)<GOAL>motive q q'
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>a b : X<GOAL>a ≈ b → f a = f b
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>Continuous (t2Quotient.lift hf)
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>x : X<GOAL>t2Quotient.lift hf (t2Quotient.mk x) = f x
<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>f : X → Y<VAR>hf : Continuous f<VAR>g : t2Quotient X → Y<VAR>hfg : g ∘ t2Quotient.mk = f<GOAL>g = t2Quotient.lift hf
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>f g : Y → X<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>IsClosed {y | f y = g y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>f g : Y → X<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>IsOpen {y | f y ≠ g y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>s : Set Y<VAR>f g : Y → X<VAR>h : Set.EqOn f g s<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Set.EqOn f g (closure s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>s : Set Y<VAR>hs : Dense s<VAR>f g : Y → X<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>h : Set.EqOn f g s<GOAL>f = g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_3<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>T2Space Z<VAR>s : Set X<VAR>t : Set Y<VAR>f g : X → Y → Z<VAR>h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y<VAR>hf₁ : ∀ (x : X), Continuous (f x)<VAR>hf₂ : ∀ (y : Y), Continuous fun x => f x y<VAR>hg₁ : ∀ (x : X), Continuous (g x)<VAR>hg₂ : ∀ (y : Y), Continuous fun x => g x y<VAR>x : X<GOAL>x ∈ closure s → ∀ y ∈ closure t, f x y = g x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>Z : Type u_3<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>T2Space Z<VAR>s : Set X<VAR>t : Set Y<VAR>f g : X → Y → Z<VAR>h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y<VAR>hf : Continuous (Function.uncurry f)<VAR>hg : Continuous (Function.uncurry g)<VAR>x : X<GOAL>x ∈ closure s → ∀ y ∈ closure t, f x y = g x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space Y<VAR>s t : Set X<VAR>f g : X → Y<VAR>h : Set.EqOn f g s<VAR>hf : ContinuousOn f t<VAR>hg : ContinuousOn g t<VAR>hst : s ⊆ t<VAR>hts : t ⊆ closure s<GOAL>Set.EqOn f g t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>T2Space X<VAR>f : X → Y<VAR>g : Y → X<VAR>h : Function.LeftInverse f g<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>IsClosed (Set.range g)