ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>h : LipschitzOnWith K f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>r : ℝ≥0∞<VAR>hr : edist x y ≤ r<GOAL>edist (f x) (f y) ≤ ↑K * r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>d : ℝ≥0∞<VAR>hd : edist x y < d / ↑K<GOAL>edist (f x) (f y) < d
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>g : β → γ<VAR>t : Set β<VAR>Kg : ℝ≥0<VAR>hg : LipschitzOnWith Kg g t<VAR>hf : LipschitzOnWith K f s<VAR>hmaps : Set.MapsTo f s t<GOAL>LipschitzOnWith (Kg * K) (g ∘ f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>s : Set α<VAR>f : α → β<VAR>g : α → γ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzOnWith Kf f s<VAR>hg : LipschitzOnWith Kg g s<GOAL>LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α → β → γ<VAR>K₁ K₂ : ℝ≥0<VAR>s : Set α<VAR>t : Set β<VAR>hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s<VAR>hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t<GOAL>EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>K : ℝ≥0<VAR>hf : LipschitzWith K f<GOAL>LocallyLipschitz f
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>LocallyLipschitz id
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>b : β<GOAL>LocallyLipschitz fun x => b
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>hf : LocallyLipschitz f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>f : β → γ<VAR>g : α → β<VAR>hf : LocallyLipschitz f<VAR>hg : LocallyLipschitz g<GOAL>LocallyLipschitz (f ∘ g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α → β<VAR>hf : LocallyLipschitz f<VAR>g : α → γ<VAR>hg : LocallyLipschitz g<GOAL>LocallyLipschitz fun x => (f x, g x)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>a : α<GOAL>LocallyLipschitz (Prod.mk a)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>b : β<GOAL>LocallyLipschitz fun a => (a, b)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → α<VAR>hf : LocallyLipschitz f<VAR>n : ℕ<GOAL>LocallyLipschitz f^[n]
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f g : Function.End α<VAR>hf : LocallyLipschitz f<VAR>hg : LocallyLipschitz g<GOAL>LocallyLipschitz (f * g)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : Function.End α<VAR>h : LocallyLipschitz f<VAR>n : ℕ<GOAL>LocallyLipschitz (f ^ n)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : LocallyLipschitzOn s f<GOAL>ContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>TopologicalSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<GOAL>ContinuousOn f (s ×ˢ t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>TopologicalSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s : Set α<VAR>t : Set β<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<GOAL>ContinuousOn f (s ×ˢ t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>TopologicalSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>hs : Dense s<VAR>ha : ∀ a ∈ s, Continuous fun y => f (a, y)<VAR>hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>TopologicalSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>K : ℝ≥0<VAR>ha : ∀ (a : α), Continuous fun y => f (a, y)<VAR>hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)<GOAL>Continuous f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>as : List α<GOAL>𝓝 as = traverse 𝓝 as
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>𝓝 [] = pure []
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>l : List α<GOAL>𝓝 (a :: l) = Seq.seq (List.cons <$> 𝓝 a) fun x => 𝓝 l
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>l : List α<GOAL>Filter.Tendsto (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l))
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>α : Type u_3<VAR>f : α → β<VAR>g : α → List β<VAR>a : Filter α<VAR>b : β<VAR>l : List β<VAR>hf : Filter.Tendsto f a (𝓝 b)<VAR>hg : Filter.Tendsto g a (𝓝 l)<GOAL>Filter.Tendsto (fun a => f a :: g a) a (𝓝 (b :: l))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>f : List α → β<VAR>b : Filter β<VAR>a : α<VAR>l : List α<GOAL>Filter.Tendsto f (𝓝 (a :: l)) b ↔ Filter.Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>Continuous fun x => x.1 :: x.2
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>f : List α → β<VAR>r : List α → Filter β<VAR>h_nil : Filter.Tendsto f (pure []) (r [])<VAR>h_cons : ∀ (l : List α) (a : α), Filter.Tendsto f (𝓝 l) (r l) → Filter.Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))<VAR>l : List α<GOAL>Filter.Tendsto f (𝓝 l) (r l)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>l : List α<GOAL>ContinuousAt List.length l
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>n : ℕ<VAR>l : List α<GOAL>Filter.Tendsto (fun p => List.insertNth n p.1 p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (List.insertNth n a l))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_3<VAR>n : ℕ<VAR>a : α<VAR>l : List α<VAR>f : β → α<VAR>g : β → List α<VAR>b : Filter β<VAR>hf : Filter.Tendsto f b (𝓝 a)<VAR>hg : Filter.Tendsto g b (𝓝 l)<GOAL>Filter.Tendsto (fun b => List.insertNth n (f b) (g b)) b (𝓝 (List.insertNth n a l))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<GOAL>Continuous fun p => List.insertNth n p.1 p.2
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>l : List α<GOAL>Filter.Tendsto (fun x => x.eraseIdx n) (𝓝 l) (𝓝 (l.eraseIdx n))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<GOAL>Continuous fun l => l.eraseIdx n
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Monoid α<VAR>ContinuousMul α<VAR>l : List α<GOAL>Filter.Tendsto List.prod (𝓝 l) (𝓝 l.prod)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>AddMonoid α<VAR>ContinuousAdd α<VAR>l : List α<GOAL>Filter.Tendsto List.sum (𝓝 l) (𝓝 l.sum)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>Monoid α<VAR>ContinuousMul α<GOAL>Continuous List.prod
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>AddMonoid α<VAR>ContinuousAdd α<GOAL>Continuous List.sum
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>a : α<VAR>l : Mathlib.Vector α n<GOAL>Filter.Tendsto (fun p => p.1 ::ᵥ p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a ::ᵥ l))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>a : α<VAR>l : Mathlib.Vector α n<GOAL>Filter.Tendsto (fun p => Mathlib.Vector.insertNth p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (Mathlib.Vector.insertNth a i l))
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>Continuous fun p => Mathlib.Vector.insertNth p.1 i p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>f : β → α<VAR>g : β → Mathlib.Vector α n<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun b => Mathlib.Vector.insertNth (f b) i (g b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>l : Mathlib.Vector α (n + 1)<GOAL>ContinuousAt (Mathlib.Vector.eraseIdx i) l
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>Continuous (Mathlib.Vector.eraseIdx i)
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>s : Set α<VAR>hs : s ∈ g<GOAL>IsOpen s
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>a : α<GOAL>𝓝 a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s
<VAR>α : Type u<VAR>β : Type u_1<VAR>m : α → β<VAR>f : Filter α<VAR>g : Set (Set β)<VAR>b : β<GOAL>Filter.Tendsto m f (𝓝 b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
<VAR>α : Type u<VAR>n : α → Filter α<VAR>ι : α → Sort u_1<VAR>p : (a : α) → ι a → Prop<VAR>s : (a : α) → ι a → Set α<VAR>hb : ∀ (a : α), (n a).HasBasis (p a) (s a)<VAR>hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i<VAR>hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x<VAR>a : α<GOAL>𝓝 a = n a
<VAR>α : Type u<VAR>n : α → Filter α<VAR>a : α<VAR>h₀ : pure ≤ n<VAR>h₁ : ∀ (a : α), ∀ s ∈ n a, ∀ᶠ (y : α) in n a, s ∈ n y<GOAL>𝓝 a = n a
<VAR>α : Type u<VAR>DecidableEq α<VAR>a₀ : α<VAR>l : Filter α<VAR>h : pure a₀ ≤ l<VAR>b : α<GOAL>𝓝 b = Function.update pure a₀ l b
<VAR>α : Type u<VAR>B : α → FilterBasis α<VAR>a : α<VAR>h₀ : ∀ (x : α), ∀ n ∈ B x, x ∈ n<VAR>h₁ : ∀ (x : α), ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n<GOAL>𝓝 a = (B a).filter
<VAR>α : Type u_1<VAR>t s : TopologicalSpace α<GOAL>t ≤ s ↔ IsOpen ≤ IsOpen
<VAR>α : Type u<VAR>g : Set (Set α)<VAR>t : TopologicalSpace α<GOAL>t ≤ TopologicalSpace.generateFrom g ↔ g ⊆ {s | IsOpen s}
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : {u | TopologicalSpace.GenerateOpen s u} = s<GOAL>TopologicalSpace.mkOfClosure s hs = TopologicalSpace.generateFrom s
<VAR>α : Type u_1<GOAL>GaloisConnection (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u_1<VAR>g₁ g₂ : Set (Set α)<VAR>h : g₁ ⊆ g₂<GOAL>TopologicalSpace.generateFrom g₂ ≤ TopologicalSpace.generateFrom g₁
<VAR>α : Type u<VAR>t : TopologicalSpace α<GOAL>TopologicalSpace.generateFrom {s | IsOpen s} = t
<VAR>α : Type u<GOAL>Function.LeftInverse TopologicalSpace.generateFrom fun t => {s | IsOpen s}
<VAR>α : Type u<GOAL>Function.Surjective TopologicalSpace.generateFrom
<VAR>α : Type u<GOAL>Function.Injective fun t => {s | IsOpen s}
<VAR>α : Type u_1<VAR>t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>hs : IsOpen s<VAR>h : t₁ ≤ t₂<GOAL>IsOpen s
<VAR>α : Type u_1<VAR>t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>h : t₁ ≤ t₂<GOAL>IsClosed s
<VAR>α : Type u_1<VAR>t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>h : t₁ ≤ t₂<GOAL>closure s ⊆ closure s
<VAR>α : Type u_1<VAR>t₁ t₂ : TopologicalSpace α<GOAL>(∀ (s : Set α), IsOpen s → IsOpen s) ↔ t₂ ≤ t₁
<VAR>α : Type u_2<VAR>U : Set α<GOAL>IsOpen U ↔ U = ∅ ∨ U = Set.univ
<VAR>α : Type u_2<VAR>t : TopologicalSpace α<VAR>self : DiscreteTopology α<GOAL>t = ⊥
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>s : Set α<GOAL>IsOpen s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>s : Set α<GOAL>IsClosed s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>s : Set α<GOAL>closure s = s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>s : Set α<GOAL>Dense s ↔ s = Set.univ
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>ι : Type u_3<VAR>f : ι → α<GOAL>DenseRange f ↔ Function.Surjective f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>f : α → β<GOAL>Continuous f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>DiscreteTopology β<VAR>f : α → β<GOAL>Continuous f ↔ ∀ (b : β), IsOpen (f ⁻¹' {b})
<VAR>α : Type u_3<VAR>TopologicalSpace α<VAR>DiscreteTopology α<GOAL>𝓝 = pure
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ x ∈ s
<VAR>α : Type u_1<VAR>t₁ t₂ : TopologicalSpace α<VAR>h : ∀ (x : α), 𝓝 x ≤ 𝓝 x<GOAL>t₁ ≤ t₂
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<VAR>h : ∀ (x : α), IsOpen {x}<GOAL>t = ⊥
<VAR>X : Type u_2<VAR>TopologicalSpace X<GOAL>(∀ (s : Set X), IsOpen s) ↔ DiscreteTopology X
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (s : Set α), IsClosed s
<VAR>X : Type u_2<VAR>TopologicalSpace X<GOAL>(∀ (a : X), IsOpen {a}) ↔ DiscreteTopology X
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (x : α), 𝓝[≠] x = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>DiscreteTopology β<VAR>f : α → β<VAR>hc : Continuous f<VAR>hinj : Function.Injective f<GOAL>DiscreteTopology α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<GOAL>IsOpen s ↔ ∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>s : Set α<VAR>f : α → β<GOAL>IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>s : Set β<VAR>f : α → β<GOAL>IsOpen s ↔ IsOpen (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>s : Set β<VAR>f : α → β<GOAL>IsClosed s ↔ IsClosed (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>a : α<VAR>hs : s ∈ 𝓝 (π a)<GOAL>π ⁻¹' s ∈ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>t' : TopologicalSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>TopologicalSpace.coinduced f t ≤ t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>tα : TopologicalSpace α<VAR>tβ : TopologicalSpace β<GOAL>TopologicalSpace.coinduced f tα ≤ tβ ↔ tα ≤ TopologicalSpace.induced f tβ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>t' : TopologicalSpace β<VAR>f : α → β<VAR>h : Continuous f<GOAL>t ≤ TopologicalSpace.induced f t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>g : β → α<VAR>h : t₁ ≤ t₂<GOAL>TopologicalSpace.induced g t₁ ≤ TopologicalSpace.induced g t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>f : α → β<VAR>h : t₁ ≤ t₂<GOAL>TopologicalSpace.coinduced f t₁ ≤ TopologicalSpace.coinduced f t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → α<GOAL>TopologicalSpace.induced g ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>g : β → α<GOAL>TopologicalSpace.induced g (t₁ ⊓ t₂) = TopologicalSpace.induced g t₁ ⊓ TopologicalSpace.induced g t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>g : β → α<VAR>ι : Sort w<VAR>t : ι → TopologicalSpace α<GOAL>TopologicalSpace.induced g (⨅ i, t i) = ⨅ i, TopologicalSpace.induced g (t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>TopologicalSpace.coinduced f ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t₁ t₂ : TopologicalSpace α<VAR>f : α → β<GOAL>TopologicalSpace.coinduced f (t₁ ⊔ t₂) = TopologicalSpace.coinduced f t₁ ⊔ TopologicalSpace.coinduced f t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ι : Sort w<VAR>t : ι → TopologicalSpace α<GOAL>TopologicalSpace.coinduced f (⨆ i, t i) = ⨆ i, TopologicalSpace.coinduced f (t i)
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<GOAL>TopologicalSpace.induced id t = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>tγ : TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<GOAL>TopologicalSpace.induced f (TopologicalSpace.induced g tγ) = TopologicalSpace.induced (g ∘ f) tγ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>x : α<GOAL>TopologicalSpace.induced (fun x_1 => x) t = ⊤
<VAR>α : Type u_1<VAR>t : TopologicalSpace α<GOAL>TopologicalSpace.coinduced id t = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>tα : TopologicalSpace α<VAR>f : α → β<VAR>g : β → γ<GOAL>TopologicalSpace.coinduced g (TopologicalSpace.coinduced f tα) = TopologicalSpace.coinduced (g ∘ f) tα
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>e : α ≃ β<GOAL>TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>e : α ≃ β<GOAL>TopologicalSpace.coinduced ⇑e.symm = TopologicalSpace.induced ⇑e
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>IsEmpty β<VAR>f : α → β<GOAL>Continuous f
<VAR>α : Type u<VAR>t : TopologicalSpace α<VAR>g : Set (Set α)<VAR>h : ∀ s ∈ g, IsOpen s<GOAL>t ≤ TopologicalSpace.generateFrom g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : Set (Set β)<VAR>f : α → β<GOAL>TopologicalSpace.induced f (TopologicalSpace.generateFrom b) = TopologicalSpace.generateFrom (Set.preimage f '' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<VAR>f : α → β<VAR>h : ∀ a ∈ b, IsOpen (f ⁻¹' a)<GOAL>t ≤ TopologicalSpace.induced f (TopologicalSpace.generateFrom b)
<VAR>α : Type u_1<VAR>s : Set (Set α)<VAR>t : Set α<VAR>ht : TopologicalSpace.GenerateOpen s t<GOAL>TopologicalSpace.generateFrom (insert t s) = TopologicalSpace.generateFrom s
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>TopologicalSpace.generateFrom (insert Set.univ s) = TopologicalSpace.generateFrom s
<VAR>α : Type u<VAR>a : α<GOAL>GaloisConnection (nhdsAdjoint a) fun t => 𝓝 a
<VAR>α : Type u<VAR>t₁ t₂ : TopologicalSpace α<VAR>a : α<VAR>h : t₁ ≤ t₂<GOAL>𝓝 a ≤ 𝓝 a
<VAR>α : Type u_1<VAR>t t' : TopologicalSpace α<GOAL>t ≤ t' ↔ ∀ (x : α), 𝓝 x ≤ 𝓝 x
<VAR>α : Type u_1<VAR>a b : α<VAR>f : Filter α<VAR>hb : b ≠ a<GOAL>IsOpen {b}
<VAR>α : Type u<VAR>a : α<VAR>f : Filter α<GOAL>𝓝 a = pure a ⊔ f
<VAR>α : Type u<VAR>a b : α<VAR>f : Filter α<VAR>h : b ≠ a<GOAL>𝓝 b = pure b
<VAR>α : Type u<VAR>a : α<VAR>f : Filter α<VAR>b : α<VAR>h : b ≠ a<GOAL>𝓝 b = pure b
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>f : Filter α<GOAL>𝓝 = Function.update pure a (pure a ⊔ f)
<VAR>α : Type u<VAR>a : α<VAR>f : Filter α<VAR>t : TopologicalSpace α<GOAL>t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b
<VAR>α : Type u_1<VAR>a : α<VAR>f : Filter α<VAR>t : TopologicalSpace α<GOAL>t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
<VAR>α : Type u<VAR>ι : Sort u_1<VAR>t : ι → TopologicalSpace α<VAR>a : α<GOAL>𝓝 a = ⨅ i, 𝓝 a
<VAR>α : Type u<VAR>s : Set (TopologicalSpace α)<VAR>a : α<GOAL>𝓝 a = ⨅ t ∈ s, 𝓝 a
<VAR>α : Type u<VAR>t₁ t₂ : TopologicalSpace α<VAR>a : α<GOAL>𝓝 a = 𝓝 a ⊓ 𝓝 a
<VAR>α : Type u<VAR>a : α<GOAL>𝓝 a = ⊤
<VAR>α : Type u<VAR>t₁ t₂ : TopologicalSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ IsOpen s ∧ IsOpen s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>t₂ : TopologicalSpace β<GOAL>Continuous f ↔ TopologicalSpace.coinduced f t₁ ≤ t₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>t₂ : TopologicalSpace β<GOAL>Continuous f ↔ t₁ ≤ TopologicalSpace.induced f t₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t : TopologicalSpace α<VAR>b : Set (Set β)<GOAL>Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t : TopologicalSpace β<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>g : γ → α<VAR>t₂ : TopologicalSpace β<VAR>t₁ : TopologicalSpace γ<GOAL>Continuous g ↔ Continuous (f ∘ g)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t : TopologicalSpace α<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>g : β → γ<VAR>t₁ : TopologicalSpace α<VAR>t₂ : TopologicalSpace γ<GOAL>Continuous g ↔ Continuous (g ∘ f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₁<VAR>h₂ : Continuous f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>t₂ t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₃<VAR>h₂ : Continuous f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<GOAL>Continuous f ↔ Continuous f ∧ Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>t₃ t₂ : TopologicalSpace β<GOAL>Continuous f → Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>T : Set (TopologicalSpace α)<VAR>t₂ : TopologicalSpace β<GOAL>Continuous f ↔ ∀ t ∈ T, Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>t₂ : Set (TopologicalSpace β)<VAR>t : TopologicalSpace β<VAR>h₁ : t ∈ t₂<VAR>hf : Continuous f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : ι → TopologicalSpace α<VAR>t₂ : TopologicalSpace β<GOAL>Continuous f ↔ ∀ (i : ι), Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>t₂ : ι → TopologicalSpace β<VAR>i : ι<VAR>h : Continuous f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>t₂ t₃ : TopologicalSpace β<GOAL>Continuous f ↔ Continuous f ∧ Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<GOAL>Continuous f → Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : Set (TopologicalSpace α)<VAR>t₂ : TopologicalSpace β<VAR>t : TopologicalSpace α<VAR>h₁ : t ∈ t₁<GOAL>Continuous f → Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t₁ : TopologicalSpace α<VAR>T : Set (TopologicalSpace β)<GOAL>Continuous f ↔ ∀ t ∈ T, Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : ι → TopologicalSpace α<VAR>t₂ : TopologicalSpace β<VAR>i : ι<GOAL>Continuous f → Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>t₂ : ι → TopologicalSpace β<GOAL>Continuous f ↔ ∀ (i : ι), Continuous f
<VAR>α : Type u<VAR>t t' : TopologicalSpace α<GOAL>Continuous id ↔ t ≤ t'
<VAR>α : Type u<VAR>t t' : TopologicalSpace α<VAR>h : t ≤ t'<GOAL>Continuous id
<VAR>α : Type u<VAR>β : Type v<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>a : β<VAR>s : Set β<GOAL>s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>a : β<GOAL>𝓝 a = Filter.comap f (𝓝 (f a))
<VAR>α : Type u<VAR>β : Type v<VAR>tα : TopologicalSpace α<VAR>tβ : TopologicalSpace β<VAR>f : β → α<GOAL>tβ = TopologicalSpace.induced f tα ↔ ∀ (b : β), 𝓝 b = Filter.comap f (𝓝 (f b))
<VAR>α : Type u<VAR>β : Type v<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>hf : Function.Surjective f<VAR>a : β<GOAL>Filter.map f (𝓝 a) = 𝓝 (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>IsOpen s ↔ s ∈ Set.preimage f '' {s | IsOpen s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>h : IsOpen s<GOAL>IsOpen (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>a : α<GOAL>Filter.map f (𝓝 a) = 𝓝[Set.range f] f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>a : α<VAR>h : Set.range f ∈ 𝓝 (f a)<GOAL>Filter.map f (𝓝 a) = 𝓝 (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<GOAL>a ∈ closure s ↔ f a ∈ closure (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : α → Prop<GOAL>Filter.Tendsto p l (𝓝 True) ↔ ∀ᶠ (x : α) in l, p x
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>Filter.Tendsto p l (𝓝 q) ↔ q → ∀ᶠ (x : α) in l, p x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>p : α → Prop<GOAL>Continuous p ↔ IsOpen {x | p x}
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ Continuous fun x => x ∈ s
<VAR>α : Type u<VAR>a₁ a₂ : Set (Set α)<GOAL>TopologicalSpace.generateFrom (a₁ ∪ a₂) = TopologicalSpace.generateFrom a₁ ⊓ TopologicalSpace.generateFrom a₂
<VAR>α : Type u<VAR>t₁ t₂ : TopologicalSpace α<GOAL>{s | IsOpen s} = {s | IsOpen s} ∩ {s | IsOpen s}
<VAR>α : Type u<VAR>ι : Sort v<VAR>f : ι → Set (Set α)<GOAL>TopologicalSpace.generateFrom (⋃ i, f i) = ⨅ i, TopologicalSpace.generateFrom (f i)
<VAR>α : Type u<VAR>ι : Sort v<VAR>t : ι → TopologicalSpace α<GOAL>{s | IsOpen s} = ⋂ i, {s | IsOpen s}