ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (fun a => s.inf' hne fun x => f x a) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.inf' hne f) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (fun a => s.inf' hne fun x => f x a) t x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (s.inf' hne f) t x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousOn (f i) t<GOAL>ContinuousOn (fun a => s.inf' hne fun x => f x a) t
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousOn (f i) t<GOAL>ContinuousOn (s.inf' hne f) t
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous fun a => s.inf' hne fun x => f x a
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous (s.inf' hne f)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (fun a => s.inf fun x => f x a) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.inf f) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (fun a => s.inf fun x => f x a) t x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (s.inf f) t x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>hs : ∀ i ∈ s, ContinuousOn (f i) t<GOAL>ContinuousOn (fun a => s.inf fun x => f x a) t
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>hs : ∀ i ∈ s, ContinuousOn (f i) t<GOAL>ContinuousOn (s.inf f) t
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous fun a => s.inf fun x => f x a
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous (s.inf f)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>self : ShrinkingLemma.PartialRefinement u s<VAR>i : ι<GOAL>IsOpen (self.toFun i)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>self : ShrinkingLemma.PartialRefinement u s<GOAL>s ⊆ ⋃ i, self.toFun i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>self : ShrinkingLemma.PartialRefinement u s<VAR>i : ι<GOAL>i ∈ self.carrier → closure (self.toFun i) ⊆ u i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>self : ShrinkingLemma.PartialRefinement u s<VAR>i : ι<GOAL>i ∉ self.carrier → self.toFun i = u i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>v : ShrinkingLemma.PartialRefinement u s<VAR>i : ι<GOAL>v.toFun i ⊆ u i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (ShrinkingLemma.PartialRefinement u s)<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<VAR>v₁ v₂ : ShrinkingLemma.PartialRefinement u s<VAR>h₁ : v₁ ∈ c<VAR>h₂ : v₂ ∈ c<VAR>i : ι<VAR>hi₁ : i ∈ v₁.carrier<VAR>hi₂ : i ∈ v₂.carrier<GOAL>v₁.toFun i = v₂.toFun i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (ShrinkingLemma.PartialRefinement u s)<VAR>i : ι<VAR>ne : c.Nonempty<GOAL>ShrinkingLemma.PartialRefinement.find c ne i ∈ c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (ShrinkingLemma.PartialRefinement u s)<VAR>i : ι<VAR>ne : c.Nonempty<GOAL>i ∈ (ShrinkingLemma.PartialRefinement.find c ne i).carrier ↔ i ∈ ShrinkingLemma.PartialRefinement.chainSupCarrier c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (ShrinkingLemma.PartialRefinement u s)<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<VAR>ne : c.Nonempty<VAR>i : ι<VAR>v : ShrinkingLemma.PartialRefinement u s<VAR>hv : v ∈ c<VAR>hi : i ∈ v.carrier<GOAL>(ShrinkingLemma.PartialRefinement.find c ne i).toFun i = v.toFun i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (ShrinkingLemma.PartialRefinement u s)<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<VAR>ne : c.Nonempty<VAR>hfin : ∀ x ∈ s, {i | x ∈ u i}.Finite<VAR>hU : s ⊆ ⋃ i, u i<VAR>v : ShrinkingLemma.PartialRefinement u s<VAR>hv : v ∈ c<GOAL>v ≤ ShrinkingLemma.PartialRefinement.chainSup c hc ne hfin hU
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>v : ShrinkingLemma.PartialRefinement u s<VAR>hs : IsClosed s<VAR>i : ι<VAR>hi : i ∉ v.carrier<GOAL>∃ v', v < v'
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>uf : ∀ x ∈ s, {i | x ∈ u i}.Finite<VAR>us : s ⊆ ⋃ i, u i<GOAL>∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>uf : ∀ x ∈ s, {i | x ∈ u i}.Finite<VAR>us : s ⊆ ⋃ i, u i<GOAL>∃ v, s ⊆ Set.iUnion v ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>u : ι → Set X<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>uf : ∀ (x : X), {i | x ∈ u i}.Finite<VAR>uU : ⋃ i, u i = Set.univ<GOAL>∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>u : ι → Set X<VAR>uo : ∀ (i : ι), IsOpen (u i)<VAR>uf : ∀ (x : X), {i | x ∈ u i}.Finite<VAR>uU : ⋃ i, u i = Set.univ<GOAL>∃ v, Set.iUnion v = Set.univ ∧ (∀ (i : ι), IsClosed (v i)) ∧ ∀ (i : ι), v i ⊆ u i
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>p : Prop<GOAL>IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>p : Prop<GOAL>IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>h : IsLocalMin f a<VAR>s : Set α<GOAL>IsLocalMinOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>h : IsLocalMax f a<VAR>s : Set α<GOAL>IsLocalMaxOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>a : α<VAR>h : IsLocalExtr f a<VAR>s : Set α<GOAL>IsLocalExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set α<VAR>hf : IsLocalMinOn f t a<VAR>h : s ⊆ t<GOAL>IsLocalMinOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set α<VAR>hf : IsLocalMaxOn f t a<VAR>h : s ⊆ t<GOAL>IsLocalMaxOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>t : Set α<VAR>hf : IsLocalExtrOn f t a<VAR>h : s ⊆ t<GOAL>IsLocalExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMinOn f s a<VAR>t : Set α<GOAL>IsLocalMinOn f (s ∩ t) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMaxOn f s a<VAR>t : Set α<GOAL>IsLocalMaxOn f (s ∩ t) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalExtrOn f s a<VAR>t : Set α<GOAL>IsLocalExtrOn f (s ∩ t) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMinOn f s a<GOAL>IsLocalMinOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMaxOn f s a<GOAL>IsLocalMaxOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsExtrOn f s a<GOAL>IsLocalExtrOn f s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMinOn f s a<VAR>hs : s ∈ 𝓝 a<GOAL>IsLocalMin f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMaxOn f s a<VAR>hs : s ∈ 𝓝 a<GOAL>IsLocalMax f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalExtrOn f s a<VAR>hs : s ∈ 𝓝 a<GOAL>IsLocalExtr f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMinOn f s a<VAR>hs : s ∈ 𝓝 a<GOAL>IsLocalMin f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsMaxOn f s a<VAR>hs : s ∈ 𝓝 a<GOAL>IsLocalMax f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsExtrOn f s a<VAR>hs : s ∈ 𝓝 a<GOAL>IsLocalExtr f a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>TopologicalSpace β<VAR>hf : IsLocalMinOn f s a<VAR>(𝓝[<] f a).NeBot<GOAL>¬𝓝 (f a) ≤ Filter.map f (𝓝[s] a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>TopologicalSpace β<VAR>hf : IsLocalMaxOn f s a<VAR>(𝓝[>] f a).NeBot<GOAL>¬𝓝 (f a) ≤ Filter.map f (𝓝[s] a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>TopologicalSpace β<VAR>hf : IsLocalExtrOn f s a<VAR>(𝓝[<] f a).NeBot<VAR>(𝓝[>] f a).NeBot<GOAL>¬𝓝 (f a) ≤ Filter.map f (𝓝[s] a)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>IsLocalMinOn (fun x => b) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>IsLocalMaxOn (fun x => b) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>IsLocalExtrOn (fun x => b) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>IsLocalMin (fun x => b) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>IsLocalMax (fun x => b) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>IsLocalExtr (fun x => b) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsLocalMin (g ∘ f) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsLocalMax (g ∘ f) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalExtr f a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsLocalExtr (g ∘ f) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsLocalMax (g ∘ f) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsLocalMin (g ∘ f) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalExtr f a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsLocalExtr (g ∘ f) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMinOn f s a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsLocalMinOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMaxOn f s a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsLocalMaxOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalExtrOn f s a<VAR>g : β → γ<VAR>hg : Monotone g<GOAL>IsLocalExtrOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMinOn f s a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsLocalMaxOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalMaxOn f s a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsLocalMinOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>hf : IsLocalExtrOn f s a<VAR>g : β → γ<VAR>hg : Antitone g<GOAL>IsLocalExtrOn (g ∘ f) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsLocalMin f a<VAR>g : α → γ<VAR>hg : IsLocalMin g a<GOAL>IsLocalMin (fun x => op (f x) (g x)) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsLocalMax f a<VAR>g : α → γ<VAR>hg : IsLocalMax g a<GOAL>IsLocalMax (fun x => op (f x) (g x)) a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsLocalMinOn f s a<VAR>g : α → γ<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMinOn (fun x => op (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>Preorder δ<VAR>op : β → γ → δ<VAR>hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op<VAR>hf : IsLocalMaxOn f s a<VAR>g : α → γ<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMaxOn (fun x => op (f x) (g x)) s a
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalMin f (g b)<VAR>hg : ContinuousAt g b<GOAL>IsLocalMin (f ∘ g) b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalMax f (g b)<VAR>hg : ContinuousAt g b<GOAL>IsLocalMax (f ∘ g) b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalExtr f (g b)<VAR>hg : ContinuousAt g b<GOAL>IsLocalExtr (f ∘ g) b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>s : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalMin f (g b)<VAR>hg : ContinuousOn g s<VAR>hb : b ∈ s<GOAL>IsLocalMinOn (f ∘ g) s b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>s : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalMax f (g b)<VAR>hg : ContinuousOn g s<VAR>hb : b ∈ s<GOAL>IsLocalMaxOn (f ∘ g) s b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>s : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalExtr f (g b)<VAR>hg : ContinuousOn g s<VAR>hb : b ∈ s<GOAL>IsLocalExtrOn (f ∘ g) s b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>t : Set α<VAR>s : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalMinOn f t (g b)<VAR>hst : s ⊆ g ⁻¹' t<VAR>hg : ContinuousOn g s<VAR>hb : b ∈ s<GOAL>IsLocalMinOn (f ∘ g) s b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>t : Set α<VAR>s : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalMaxOn f t (g b)<VAR>hst : s ⊆ g ⁻¹' t<VAR>hg : ContinuousOn g s<VAR>hb : b ∈ s<GOAL>IsLocalMaxOn (f ∘ g) s b
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type x<VAR>TopologicalSpace α<VAR>Preorder β<VAR>f : α → β<VAR>TopologicalSpace δ<VAR>t : Set α<VAR>s : Set δ<VAR>g : δ → α<VAR>b : δ<VAR>hf : IsLocalExtrOn f t (g b)<VAR>hst : s ⊆ g ⁻¹' t<VAR>hg : ContinuousOn g s<VAR>hb : b ∈ s<GOAL>IsLocalExtrOn (f ∘ g) s b
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>hg : IsLocalMin g a<GOAL>IsLocalMin (fun x => f x + g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>hg : IsLocalMax g a<GOAL>IsLocalMax (fun x => f x + g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMinOn (fun x => f x + g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommMonoid β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMaxOn (fun x => f x + g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<GOAL>IsLocalMax (fun x => -f x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<GOAL>IsLocalMin (fun x => -f x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>hf : IsLocalExtr f a<GOAL>IsLocalExtr (fun x => -f x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<GOAL>IsLocalMaxOn (fun x => -f x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<GOAL>IsLocalMinOn (fun x => -f x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalExtrOn f s a<GOAL>IsLocalExtrOn (fun x => -f x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>hg : IsLocalMax g a<GOAL>IsLocalMin (fun x => f x - g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>hg : IsLocalMin g a<GOAL>IsLocalMax (fun x => f x - g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMinOn (fun x => f x - g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMaxOn (fun x => f x - g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>hg : IsLocalMin g a<GOAL>IsLocalMin (fun x => f x ⊔ g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>hg : IsLocalMax g a<GOAL>IsLocalMax (fun x => f x ⊔ g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMinOn (fun x => f x ⊔ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeSup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMaxOn (fun x => f x ⊔ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>hg : IsLocalMin g a<GOAL>IsLocalMin (fun x => f x ⊓ g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMax f a<VAR>hg : IsLocalMax g a<GOAL>IsLocalMax (fun x => f x ⊓ g x) a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMinOn f s a<VAR>hg : IsLocalMinOn g s a<GOAL>IsLocalMinOn (fun x => f x ⊓ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SemilatticeInf β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>hf : IsLocalMaxOn f s a<VAR>hg : IsLocalMaxOn g s a<GOAL>IsLocalMaxOn (fun x => f x ⊓ g x) s a
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>LinearOrder β<VAR>f g : α → β<VAR>a : α<VAR>hf : IsLocalMin f a<VAR>hg : IsLocalMin g a<GOAL>IsLocalMin (fun x => min (f x) (g x)) a