ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hg : Continuous g<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (g ∘ f) s
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>s : Set α<VAR>hg : Continuous g<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => g (f x)) 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>hg : ContinuousOn g s<VAR>hf : Continuous f<VAR>hs : ∀ (x : α), f x ∈ s<GOAL>Continuous (g ∘ f)
<VAR>ι : Type u_7<VAR>π : ι → Type u_8<VAR>(i : ι) → TopologicalSpace (π i)<VAR>i : ι<VAR>s : Set ((i : ι) → π i)<GOAL>ContinuousOn (fun p => p i) s
<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 : t ∈ 𝓝 (f x)<GOAL>f ⁻¹' t ∈ 𝓝[s] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>g : β → α<VAR>x : β<VAR>s : Set β<VAR>h : Set.LeftInvOn f g s<VAR>hx : f (g x) = x<VAR>hf : ContinuousWithinAt f (g '' s) (g x)<VAR>hg : ContinuousWithinAt g s x<GOAL>Filter.map g (𝓝[s] x) = 𝓝[g '' s] g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>g : β → α<VAR>x : β<VAR>h : Function.LeftInverse f g<VAR>hf : ContinuousWithinAt f (Set.range g) (g x)<VAR>hg : ContinuousAt g x<GOAL>Filter.map g (𝓝 x) = 𝓝[Set.range g] g x
<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 : t ∈ 𝓝[f '' s] f x<GOAL>f ⁻¹' t ∈ 𝓝[s] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>x : α<VAR>y : β<VAR>s t : Set β<VAR>h : ContinuousWithinAt f (f ⁻¹' s) x<VAR>ht : t ∈ 𝓝[s] y<VAR>hxy : y = f x<GOAL>f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>s : Set α<VAR>x : α<VAR>h : f =ᶠ[𝓝[s] x] g<VAR>hx : f x = g x<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f f₁ : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>ContinuousWithinAt f₁ s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f f₁ : α → β<VAR>s : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<VAR>hx : f₁ x = f x<GOAL>ContinuousWithinAt f₁ s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f g : α → β<VAR>s s₁ : Set α<VAR>x : α<VAR>h : ContinuousWithinAt f s x<VAR>h' : Set.EqOn g f s₁<VAR>h₁ : s₁ ⊆ s<VAR>hx : g x = f x<GOAL>ContinuousWithinAt g s₁ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>c : β<GOAL>ContinuousOn (fun x => c) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>b : β<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt (fun x => b) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>ContinuousOn id s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>ContinuousOn (fun x => x) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt id s 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 ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)
<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>hs : IsOpen s<VAR>ht : IsOpen t<GOAL>IsOpen (s ∩ f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>h : ContinuousOn f s<VAR>hs : IsOpen s<VAR>hp : f ⁻¹' t ⊆ s<VAR>ht : IsOpen t<GOAL>IsOpen (f ⁻¹' t)
<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>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>IsClosed (s ∩ f ⁻¹' t)
<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>hs : IsOpen s<GOAL>s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>s : Set α<VAR>T : Set (Set β)<VAR>f : α → β<GOAL>ContinuousOn f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_7<VAR>s : Set α<VAR>T : Set (Set β)<VAR>f : α → β<VAR>h : ∀ t ∈ T, IsOpen (s ∩ f ⁻¹' t)<GOAL>ContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : α → γ<VAR>s : Set α<VAR>x : α<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun x => (f x, g x)) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : α → γ<VAR>s : Set α<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => (f x, g x)) 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>h : α → γ<VAR>x : α<VAR>s : Set α<VAR>hf : ContinuousAt f (g x, h x)<VAR>hg : ContinuousWithinAt g s x<VAR>hh : ContinuousWithinAt h s x<GOAL>ContinuousWithinAt (fun x => f (g x, h x)) s 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>h : α → γ<VAR>x : α<VAR>s : Set α<VAR>y : β × γ<VAR>hf : ContinuousAt f y<VAR>hg : ContinuousWithinAt g s x<VAR>hh : ContinuousWithinAt h s x<VAR>e : (g x, h x) = y<GOAL>ContinuousWithinAt (fun x => f (g x, h x)) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Inducing g<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Inducing g<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hg : Embedding g<VAR>s : Set α<GOAL>ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : Embedding f<VAR>s : Set α<VAR>x : α<GOAL>Filter.map f (𝓝[s] x) = 𝓝[f '' s] f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>hf : OpenEmbedding f<VAR>s : Set β<VAR>x : α<GOAL>Filter.map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>h : QuotientMap f<VAR>s : Set β<VAR>hs : IsOpen s<GOAL>ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : α → β<VAR>s : Set α<VAR>x : α<VAR>hx : x ∉ closure s<GOAL>ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>p : α → Prop<VAR>f g : α → β<VAR>(a : α) → Decidable (p a)<VAR>hpf : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))<VAR>hpg : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))<VAR>hf : ContinuousOn f (s ∩ {a | p a})<VAR>hg : ContinuousOn g (s ∩ {a | ¬p a})<GOAL>ContinuousOn (fun a => if p a then f a else g a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s t : Set α<VAR>f g : α → β<VAR>(a : α) → Decidable (a ∈ t)<VAR>hpf : ∀ a ∈ s ∩ frontier t, Filter.Tendsto f (𝓝[s ∩ t] a) (𝓝 (t.piecewise f g a))<VAR>hpg : ∀ a ∈ s ∩ frontier t, Filter.Tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (t.piecewise f g a))<VAR>hf : ContinuousOn f (s ∩ t)<VAR>hg : ContinuousOn g (s ∩ tᶜ)<GOAL>ContinuousOn (t.piecewise f g) s
<VAR>α : Type u_7<VAR>β : Type u_8<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>p : α → Prop<VAR>(a : α) → Decidable (p a)<VAR>s : Set α<VAR>f g : α → β<VAR>hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure {a | p a})<VAR>hg : ContinuousOn g (s ∩ closure {a | ¬p a})<GOAL>ContinuousOn (fun a => if p a then f a else g a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s t : Set α<VAR>f g : α → β<VAR>(a : α) → Decidable (a ∈ t)<VAR>ht : ∀ a ∈ s ∩ frontier t, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure t)<VAR>hg : ContinuousOn g (s ∩ closure tᶜ)<GOAL>ContinuousOn (t.piecewise f g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>p : α → Prop<VAR>f g : α → β<VAR>(a : α) → Decidable (p a)<VAR>hpf : ∀ a ∈ frontier {x | p x}, Filter.Tendsto f (𝓝[{x | p x}] a) (𝓝 (if p a then f a else g a))<VAR>hpg : ∀ a ∈ frontier {x | p x}, Filter.Tendsto g (𝓝[{x | ¬p x}] a) (𝓝 (if p a then f a else g a))<VAR>hf : ContinuousOn f {x | p x}<VAR>hg : ContinuousOn g {x | ¬p x}<GOAL>Continuous fun a => if p a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>p : α → Prop<VAR>f g : α → β<VAR>(a : α) → Decidable (p a)<VAR>hp : ∀ a ∈ frontier {x | p x}, f a = g a<VAR>hf : ContinuousOn f (closure {x | p x})<VAR>hg : ContinuousOn g (closure {x | ¬p x})<GOAL>Continuous fun a => if p a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>p : α → Prop<VAR>f g : α → β<VAR>(a : α) → Decidable (p a)<VAR>hp : ∀ a ∈ frontier {x | p x}, f a = g a<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun a => if p a then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>p : Prop<VAR>f g : α → β<VAR>Decidable p<VAR>hf : p → Continuous f<VAR>hg : ¬p → Continuous g<GOAL>Continuous fun a => if p then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>p : Prop<VAR>f g : α → β<VAR>Decidable p<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun a => if p then f a else g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>f g : α → β<VAR>(a : α) → Decidable (a ∈ s)<VAR>hs : ∀ a ∈ frontier s, f a = g a<VAR>hf : ContinuousOn f (closure s)<VAR>hg : ContinuousOn g (closure sᶜ)<GOAL>Continuous (s.piecewise f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set α<VAR>f g : α → β<VAR>(a : α) → Decidable (a ∈ s)<VAR>hs : ∀ a ∈ frontier s, f a = g a<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (s.piecewise f g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α → β<VAR>s : Set α<VAR>hs : ∀ a ∈ frontier s, f a = 0<VAR>hf : ContinuousOn f (closure s)<GOAL>Continuous (s.indicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>One β<VAR>f : α → β<VAR>s : Set α<VAR>hs : ∀ a ∈ frontier s, f a = 1<VAR>hf : ContinuousOn f (closure s)<GOAL>Continuous (s.mulIndicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>One β<VAR>f : α → β<VAR>s : Set α<VAR>hs : ∀ a ∈ frontier s, f a = 1<VAR>hf : Continuous f<GOAL>Continuous (s.mulIndicator f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>f : α → β<VAR>s : Set α<VAR>hs : ∀ a ∈ frontier s, f a = 0<VAR>hf : Continuous f<GOAL>Continuous (s.indicator f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s s' t : Set α<VAR>hs : IsOpen s<VAR>hs' : IsOpen s'<VAR>ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'<GOAL>IsOpen (t.ite s s')
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s s' t : Set α<VAR>hs : IsOpen s<VAR>hs' : IsOpen s'<VAR>ht : s ∩ frontier t = s' ∩ frontier t<GOAL>IsOpen (t.ite s s')
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s s' t : Set α<VAR>ht : s ∩ frontier t = s' ∩ frontier t<GOAL>t.ite s s' ∩ closure t = s ∩ closure t
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s s' t : Set α<VAR>ht : s ∩ frontier t = s' ∩ frontier t<GOAL>t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s s' t : Set α<VAR>f f' : α → β<VAR>(x : α) → Decidable (x ∈ t)<VAR>h : ContinuousOn f (s ∩ closure t)<VAR>h' : ContinuousOn f' (s' ∩ closure tᶜ)<VAR>H : s ∩ frontier t = s' ∩ frontier t<VAR>Heq : Set.EqOn f f' (s ∩ frontier t)<GOAL>ContinuousOn (t.piecewise f f') (t.ite s s')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s s' t : Set α<VAR>f f' : α → β<VAR>(x : α) → Decidable (x ∈ t)<VAR>h : ContinuousOn f s<VAR>h' : ContinuousOn f' s'<VAR>H : s ∩ frontier t = s' ∩ frontier t<VAR>Heq : Set.EqOn f f' (s ∩ frontier t)<GOAL>ContinuousOn (t.piecewise f f') (t.ite s s')
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s t : Set α<VAR>ht : IsOpen t<GOAL>frontier (s ∩ t) ∩ t = frontier s ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (α × β)<GOAL>ContinuousOn Prod.fst s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (α × β)<VAR>p : α × β<GOAL>ContinuousWithinAt Prod.fst s p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β × γ<VAR>s : Set α<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => (f x).1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β × γ<VAR>s : Set α<VAR>a : α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => (f x).1) s a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (α × β)<GOAL>ContinuousOn Prod.snd s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>s : Set (α × β)<VAR>p : α × β<GOAL>ContinuousWithinAt Prod.snd s p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β × γ<VAR>s : Set α<VAR>hf : ContinuousOn f s<GOAL>ContinuousOn (fun x => (f x).2) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β × γ<VAR>s : Set α<VAR>a : α<VAR>h : ContinuousWithinAt f s a<GOAL>ContinuousWithinAt (fun x => (f x).2) s a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : α → β × γ<VAR>s : Set α<VAR>x : α<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>LipschitzOnWith K f ∅
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<GOAL>LocallyLipschitzOn ∅ f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s t : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f t<VAR>h : s ⊆ t<GOAL>LipschitzOnWith K f s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>s t : Set α<VAR>f : α → β<VAR>hf : LocallyLipschitzOn t f<VAR>h : s ⊆ t<GOAL>LocallyLipschitzOn s f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>LipschitzOnWith K f Set.univ ↔ LipschitzWith K f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<GOAL>LocallyLipschitzOn Set.univ f ↔ LocallyLipschitz f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<GOAL>LipschitzOnWith K f s ↔ LipschitzWith K (s.restrict f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>t : Set ↑s<GOAL>LipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>s : Set α<VAR>f : α → β<GOAL>LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>t : Set β<VAR>h : Set.MapsTo f s t<GOAL>LipschitzOnWith K f s ↔ LipschitzWith K (Set.MapsTo.restrict f s t h)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>h : LipschitzWith K f<VAR>s : Set α<GOAL>LipschitzOnWith K f s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>h : LipschitzWith K f<VAR>x y : α<GOAL>edist (f x) (f y) ≤ ↑K * edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>h : LipschitzWith K f<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>f : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>h : LipschitzWith K f<VAR>hK : K ≠ 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>f : α → β<VAR>h : LipschitzWith K f<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>Set.MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) (↑K * r))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>h : LipschitzWith K f<VAR>hK : K ≠ 0<VAR>x : α<VAR>r : ℝ≥0∞<GOAL>Set.MapsTo f (EMetric.ball x r) (EMetric.ball (f x) (↑K * r))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>x y : α<VAR>h : edist x y ≠ ⊤<GOAL>edist (f x) (f y) < ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>h : LipschitzWith K f<VAR>x y : α<GOAL>(↑K)⁻¹ * edist (f x) (f y) ≤ edist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>f : α → β<VAR>h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y<GOAL>LipschitzWith 1 f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>K' : ℝ≥0<VAR>h : K ≤ K'<GOAL>LipschitzWith K' f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>s : Set α<GOAL>EMetric.diam (f '' s) ≤ ↑K * EMetric.diam s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>x y : α<VAR>d : ℝ≥0∞<VAR>h : edist x y < d / ↑K<GOAL>edist (f x) (f y) < d
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<GOAL>UniformContinuous f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<GOAL>Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>b : β<GOAL>LipschitzWith 0 fun x => b
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>b : β<VAR>K : ℝ≥0<GOAL>LipschitzWith K fun x => b
<VAR>α : Type u<VAR>PseudoEMetricSpace α<GOAL>LipschitzWith 1 id
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>s : Set α<GOAL>LipschitzWith 1 Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>p : β → Prop<VAR>hp : ∀ (x : α), p (f x)<GOAL>LipschitzWith K fun x => ⟨f x, ⋯⟩
<VAR>ι : Type x<VAR>α : ι → Type u<VAR>(i : ι) → PseudoEMetricSpace (α i)<VAR>Fintype ι<VAR>i : ι<GOAL>LipschitzWith 1 (Function.eval i)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>s : Set α<GOAL>LipschitzWith K (s.restrict f)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>Kf Kg : ℝ≥0<VAR>f : β → γ<VAR>g : α → β<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf * Kg) (f ∘ g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>Kf Kg : ℝ≥0<VAR>f : β → γ<VAR>g : α → β<VAR>s : Set α<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzOnWith Kg g s<GOAL>LipschitzOnWith (Kf * Kg) (f ∘ g) s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>LipschitzWith 1 Prod.fst
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<GOAL>LipschitzWith 1 Prod.snd
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α → β<VAR>Kf : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>g : α → γ<VAR>Kg : ℝ≥0<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (max Kf Kg) fun x => (f x, g x)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>a : α<GOAL>LipschitzWith 1 (Prod.mk a)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>b : β<GOAL>LipschitzWith 1 fun a => (a, b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>PseudoEMetricSpace γ<VAR>f : α → β → γ<VAR>Kα Kβ : ℝ≥0<VAR>hα : ∀ (b : β), LipschitzWith Kα fun a => f a b<VAR>hβ : ∀ (a : α), LipschitzWith Kβ (f a)<GOAL>LipschitzWith (Kα + Kβ) (Function.uncurry f)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>n : ℕ<GOAL>LipschitzWith (K ^ n) f^[n]
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>x : α<VAR>n : ℕ<GOAL>edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f g : Function.End α<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (Kf * Kg) (f * g)
<VAR>α : Type u<VAR>ι : Type x<VAR>PseudoEMetricSpace α<VAR>f : ι → Function.End α<VAR>K : ι → ℝ≥0<VAR>h : ∀ (i : ι), LipschitzWith (K i) (f i)<VAR>l : List ι<GOAL>LipschitzWith (List.map K l).prod (List.map f l).prod
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : Function.End α<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>n : ℕ<GOAL>LipschitzWith (K ^ n) (f ^ n)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<GOAL>UniformContinuousOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoEMetricSpace α<VAR>PseudoEMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<GOAL>ContinuousOn f s