ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_5<VAR>Finite ι<VAR>s : ι → Set α<VAR>a : α<GOAL>𝓝[⋃ i, s i] a = ⨆ i, 𝓝[s i] 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>a : α<VAR>s t : Set α<GOAL>𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : s ∈ 𝓝[t] a<GOAL>𝓝[s ∩ t] a = 𝓝[t] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : t ∈ 𝓝[s] a<GOAL>𝓝[s ∩ t] a = 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<GOAL>𝓝[{a}] a = pure a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<GOAL>t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : t ∈ 𝓝[s] a<GOAL>insert a t ∈ 𝓝[insert a s] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>a : α<GOAL>𝓝[≠] a ⊔ pure a = 𝓝 a
<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>β : Type u_6<VAR>TopologicalSpace β<VAR>s u : Set α<VAR>t v : Set β<VAR>a : α<VAR>b : β<VAR>hu : u ∈ 𝓝[s] a<VAR>hv : v ∈ 𝓝[t] b<GOAL>u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[I.pi s] x = ⨅ i, Filter.comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[I.pi s] x = (⨅ i ∈ I, Filter.comap (fun x => x i) (𝓝[s i] x i)) ⊓ ⨅ i, ⨅ (_ : i ∉ I), Filter.comap (fun x => x i) (𝓝 (x i))
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>Finite ι<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[Set.univ.pi s] x = ⨅ i, Filter.comap (fun x => x i) (𝓝[s i] x i)
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>𝓝[I.pi s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥
<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>(i : ι) → TopologicalSpace (π i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (π i)<VAR>x : (i : ι) → π i<GOAL>(𝓝[I.pi s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f g : α → β<VAR>t : Set α<VAR>(x : α) → Decidable (x ∈ t)<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h₀ : Filter.Tendsto f (𝓝[s ∩ t] a) l<VAR>h₁ : Filter.Tendsto g (𝓝[s ∩ tᶜ] a) l<GOAL>Filter.Tendsto (t.piecewise f g) (𝓝[s] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f g : α → β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h₀ : Filter.Tendsto f (𝓝[s ∩ {x | p x}] a) l<VAR>h₁ : Filter.Tendsto g (𝓝[s ∩ {x | ¬p x}] a) l<GOAL>Filter.Tendsto (fun x => if p x then f x else g x) (𝓝[s] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f : α → β<VAR>a : α<VAR>s : Set α<GOAL>Filter.map f (𝓝[s] a) = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, 𝓟 (f '' (t ∩ s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f : α → β<VAR>a : α<VAR>s t : Set α<VAR>l : Filter β<VAR>hst : s ⊆ t<VAR>h : Filter.Tendsto f (𝓝[t] a) l<GOAL>Filter.Tendsto f (𝓝[s] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f : β → α<VAR>l : Filter β<VAR>a : α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>h : Filter.Tendsto f l (𝓝[s] a)<GOAL>Filter.Tendsto f l (𝓝[t] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h : Filter.Tendsto f (𝓝 a) l<GOAL>Filter.Tendsto f (𝓝[s] a) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h : Filter.Tendsto f l (𝓝[s] a)<GOAL>∀ᶠ (i : β) in l, f i ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f : β → α<VAR>a : α<VAR>s : Set α<VAR>l : Filter β<VAR>h : Filter.Tendsto f l (𝓝[s] a)<GOAL>Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<GOAL>(𝓝[s] x).NeBot
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : IsClosed s<VAR>x : α<VAR>hx : (𝓝[s] x).NeBot<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_7<VAR>f : ι → α<VAR>h : DenseRange f<VAR>x : α<GOAL>(𝓝[Set.range f] x).NeBot
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (α i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (α i)<VAR>x : (i : ι) → α i<GOAL>x ∈ closure (I.pi s) ↔ ∀ i ∈ I, x i ∈ closure (s i)
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (α i)<VAR>I : Set ι<VAR>s : (i : ι) → Set (α i)<GOAL>closure (I.pi s) = I.pi fun i => closure (s i)
<VAR>ι : Type u_7<VAR>α : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (α i)<VAR>s : (i : ι) → Set (α i)<VAR>I : Set ι<VAR>hs : ∀ i ∈ I, Dense (s i)<GOAL>Dense (I.pi s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f g : α → β<VAR>s : Set α<VAR>a : α<GOAL>f =ᶠ[𝓝[s] a] g ↔ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → f x = g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f g : α → β<VAR>s : Set α<VAR>a : α<VAR>h : Set.EqOn f g s<GOAL>f =ᶠ[𝓝[s] a] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>f g : α → β<VAR>s : Set α<VAR>a : α<VAR>l : Filter β<VAR>hfg : ∀ x ∈ s, f x = g x<VAR>hf : Filter.Tendsto f (𝓝[s] a) l<GOAL>Filter.Tendsto g (𝓝[s] a) l
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : α<VAR>p : α → Prop<VAR>h : ∀ x ∈ s, p x<GOAL>∀ᶠ (x : α) in 𝓝[s] a, p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>a : α<VAR>l : Filter β<VAR>s : Set α<VAR>f : β → α<VAR>h1 : Filter.Tendsto f l (𝓝 a)<VAR>h2 : ∀ᶠ (x : β) in l, f x ∈ s<GOAL>Filter.Tendsto f l (𝓝[s] a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>a : α<VAR>l : Filter β<VAR>s : Set α<VAR>f : β → α<GOAL>Filter.Tendsto f l (𝓝[s] a) ↔ Filter.Tendsto f l (𝓝 a) ∧ ∀ᶠ (n : β) in l, f n ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>a : α<VAR>l : Filter β<VAR>f : β → α<GOAL>Filter.Tendsto f l (𝓝[Set.range f] a) ↔ Filter.Tendsto f l (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>f g : α → β<VAR>a : α<VAR>h : f =ᶠ[𝓝[s] a] g<VAR>hmem : a ∈ s<GOAL>f a = g a
<VAR>α : Type u_7<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : α<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in 𝓝 a, p x<GOAL>∀ᶠ (x : α) in 𝓝[s] a, p x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : { x // x ∈ s }<VAR>t u : Set { x // x ∈ s }<GOAL>t ∈ 𝓝[u] a ↔ t ∈ Filter.comap Subtype.val (𝓝[Subtype.val '' u] ↑a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : { x // x ∈ s }<VAR>t : Set { x // x ∈ s }<GOAL>𝓝[t] a = Filter.comap Subtype.val (𝓝[Subtype.val '' t] ↑a)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>𝓝[s] a = Filter.map Subtype.val (𝓝 ⟨a, h⟩)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : ↑s<VAR>t : Set ↑s<GOAL>t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>a : ↑s<GOAL>Subtype.val ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : ↑s<VAR>P : α → Prop<GOAL>(∀ᶠ (x : ↑s) in 𝓝 a, P ↑x) ↔ ∀ᶠ (x : α) in 𝓝[s] ↑a, P x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : ↑s<VAR>P : α → Prop<GOAL>(∃ᶠ (x : ↑s) in 𝓝 a, P ↑x) ↔ ∃ᶠ (x : α) in 𝓝[s] ↑a, P x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto f (𝓝[s] a) l ↔ Filter.Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<GOAL>Filter.Tendsto f (𝓝[s] x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousOn f s<VAR>hx : x ∈ s<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<GOAL>ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<GOAL>Continuous f ↔ ContinuousOn f Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>h : x ∈ s<GOAL>ContinuousWithinAt f s x ↔ ContinuousAt (s.restrict f) ⟨x, h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>t : Set β<VAR>h : ContinuousWithinAt f s x<VAR>ht : Set.MapsTo f s t<GOAL>Filter.Tendsto f (𝓝[s] x) (𝓝[t] f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<VAR>h : ContinuousWithinAt f s x<GOAL>Filter.Tendsto f (𝓝[s] x) (𝓝[f '' s] f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>f : α → γ<VAR>g : β → δ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g t y<GOAL>ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x.1, x_1)) {b | (x.1, b) ∈ s} x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<VAR>x : α × β<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 => f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology α<VAR>f : α × β → γ<VAR>x : α × β<GOAL>ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x.1, x_1)) x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology β<VAR>f : α × β → γ<VAR>x : α × β<GOAL>ContinuousAt f x ↔ ContinuousAt (fun x_1 => f (x_1, x.2)) x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology α<VAR>f : α × β → γ<VAR>s : Set (α × β)<GOAL>ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) {b | (a, b) ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology β<VAR>f : α × β → γ<VAR>s : Set (α × β)<GOAL>ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) {a | (a, b) ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology α<VAR>f : α × β → γ<GOAL>Continuous f ↔ ∀ (a : α), Continuous fun x => f (a, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology β<VAR>f : α × β → γ<GOAL>Continuous f ↔ ∀ (b : β), Continuous fun x => f (x, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology α<VAR>f : α × β → γ<GOAL>IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x => f (a, x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>DiscreteTopology β<VAR>f : α × β → γ<GOAL>IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x => f (x, b)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_7<VAR>π : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (π i)<VAR>f : α → (i : ι) → π i<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt f s x ↔ ∀ (i : ι), ContinuousWithinAt (fun y => f y i) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_7<VAR>π : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (π i)<VAR>f : α → (i : ι) → π i<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ (i : ι), ContinuousOn (fun y => f y i) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_7<VAR>π : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (π i)<VAR>f : α → (i : ι) → π i<VAR>s : Set α<VAR>hf : ∀ (i : ι), ContinuousOn (fun y => f y i) s<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>π : Fin (n + 1) → Type u_7<VAR>(i : Fin (n + 1)) → TopologicalSpace (π i)<VAR>i : Fin (n + 1)<VAR>f : α → π i<VAR>a : α<VAR>s : Set α<VAR>hf : ContinuousWithinAt f s a<VAR>g : α → (j : Fin n) → π (i.succAbove j)<VAR>hg : ContinuousWithinAt g s a<GOAL>ContinuousWithinAt (fun a => i.insertNth (f a) (g a)) s a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>n : ℕ<VAR>π : Fin (n + 1) → Type u_7<VAR>(i : Fin (n + 1)) → TopologicalSpace (π i)<VAR>i : Fin (n + 1)<VAR>f : α → π i<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>g : α → (j : Fin n) → π (i.succAbove j)<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun a => i.insertNth (f a) (g a)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ Continuous (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : ContinuousOn f s<VAR>ht : Set.MapsTo f s t<GOAL>Continuous (Set.MapsTo.restrict f s t ht)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>t₁ t₂ : TopologicalSpace α<VAR>t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₁<VAR>s : Set α<VAR>f : α → β<VAR>h₂ : ContinuousOn f s<GOAL>ContinuousOn f s
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>t₁ : TopologicalSpace α<VAR>t₂ t₃ : TopologicalSpace β<VAR>h₁ : t₂ ≤ t₃<VAR>s : Set α<VAR>f : α → β<VAR>h₂ : ContinuousOn f s<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>TopologicalSpace δ<VAR>f : α → γ<VAR>g : β → δ<VAR>s : Set α<VAR>t : Set β<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g t<GOAL>ContinuousOn (Prod.map f g) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ι : Sort u_7<VAR>f : α → β<VAR>s : ι → Set α<VAR>hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x<VAR>hf : ∀ (i : ι), ContinuousOn f (s i)<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<GOAL>ContinuousOn f ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>a : α<GOAL>ContinuousOn f {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>f : α → β<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>x : α<VAR>s : Set α<VAR>f : α → β<VAR>ctsf : ContinuousWithinAt f s x<GOAL>𝓝[s] x ≤ Filter.comap f (𝓝[f '' s] f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f t x<VAR>hs : s ⊆ t<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f t x<VAR>hs : t ∈ 𝓝[s] x<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : 𝓝[s] x = 𝓝[t] x<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : t ∈ 𝓝[s] x<GOAL>ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>h : t ∈ 𝓝 x<GOAL>ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<GOAL>ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>hs : ContinuousWithinAt f s x<VAR>ht : ContinuousWithinAt f t x<GOAL>ContinuousWithinAt f (s ∪ t) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<VAR>hx : x ∈ closure s<GOAL>f x ∈ closure (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>A : Set β<VAR>h : ContinuousWithinAt f s x<VAR>hx : x ∈ closure s<VAR>hA : Set.MapsTo f s A<GOAL>f x ∈ closure A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : Set.MapsTo f s t<VAR>hc : ∀ x ∈ closure s, ContinuousWithinAt f s x<GOAL>Set.MapsTo f (closure s) (closure t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : Set.MapsTo f s t<VAR>hc : ContinuousOn f (closure s)<GOAL>Set.MapsTo f (closure s) (closure t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : ∀ x ∈ closure s, ContinuousWithinAt f s x<GOAL>f '' closure s ⊆ closure (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hf : ContinuousOn f (closure s)<GOAL>f '' closure s ⊆ closure (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<GOAL>ContinuousWithinAt f {x} x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<VAR>s : Set α<GOAL>ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>ht : ContinuousWithinAt f t x<GOAL>ContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>a : α<GOAL>ContinuousWithinAt f {a}ᶜ a ↔ ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>DecidableEq α<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>y : β<GOAL>ContinuousWithinAt (Function.update f x y) s x ↔ Filter.Tendsto f (𝓝[s \ {x}] x) (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>DecidableEq α<VAR>f : α → β<VAR>x : α<VAR>y : β<GOAL>ContinuousAt (Function.update f x y) x ↔ Filter.Tendsto f (𝓝[≠] x) (𝓝 y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : IsOpenMap (s.restrict f)<VAR>finv : β → α<VAR>hleft : Set.LeftInvOn finv f s<GOAL>ContinuousOn finv (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : IsOpenMap f<VAR>finv : β → α<VAR>hleft : Function.LeftInverse finv f<GOAL>ContinuousOn finv (Set.range f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>s s₁ : Set α<VAR>h : ContinuousOn f s<VAR>h' : Set.EqOn g f s₁<VAR>h₁ : s₁ ⊆ s<GOAL>ContinuousOn g s₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>s : Set α<VAR>h : ContinuousOn f s<VAR>h' : Set.EqOn g f s<GOAL>ContinuousOn g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>s : Set α<VAR>h' : Set.EqOn g f s<GOAL>ContinuousOn g s ↔ ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousAt f x<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : s ∈ 𝓝 x<GOAL>ContinuousWithinAt f s x ↔ ContinuousAt f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<VAR>hs : s ∈ 𝓝 x<GOAL>ContinuousAt f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>ContinuousOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ContinuousAt f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousOn f s<VAR>hx : s ∈ 𝓝 x<GOAL>ContinuousAt f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hcont : ∀ x ∈ s, ContinuousAt f x<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>hg : ContinuousWithinAt g t (f x)<VAR>hf : ContinuousWithinAt f s x<VAR>h : Set.MapsTo f s t<GOAL>ContinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>hg : ContinuousWithinAt g t (f x)<VAR>hf : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hg : ContinuousAt g (f x)<VAR>hf : ContinuousWithinAt f s x<GOAL>ContinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : ContinuousOn g t<VAR>hf : ContinuousOn f s<VAR>h : Set.MapsTo f s t<GOAL>ContinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : ContinuousOn g t<VAR>hf : ContinuousOn f s<VAR>h : Set.MapsTo f s t<GOAL>ContinuousOn (fun x => g (f x)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s t : Set α<VAR>hf : ContinuousOn f s<VAR>h : t ⊆ s<GOAL>ContinuousOn f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<GOAL>Antitone (ContinuousOn f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hg : ContinuousOn g t<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : Continuous f<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>h : Continuous f<GOAL>ContinuousWithinAt f s x