ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace.NoetherianSpace α<VAR>f : α → β<VAR>hf : Continuous f<GOAL>TopologicalSpace.NoetherianSpace ↑(Set.range f)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<GOAL>TopologicalSpace.NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t
<VAR>α : Type u_1<VAR>TopologicalSpace α<GOAL>TopologicalSpace.NoetherianSpace ↑Set.univ ↔ TopologicalSpace.NoetherianSpace α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>f : ι → Set α<VAR>Finite ι<VAR>hf : ∀ (i : ι), TopologicalSpace.NoetherianSpace ↑(f i)<GOAL>TopologicalSpace.NoetherianSpace ↑(⋃ i, f i)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>T2Space α<GOAL>DiscreteTopology α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>T2Space α<GOAL>Finite α
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>∃ S, S.Finite ∧ (∀ t ∈ S, IsClosed t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>s : TopologicalSpace.Closeds α<GOAL>∃ S, (∀ (k : { x // x ∈ S }), IsIrreducible ↑↑k) ∧ s = S.sup id
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<GOAL>(irreducibleComponents α).Finite
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>TopologicalSpace.NoetherianSpace α<VAR>Z : Set α<VAR>H : Z ∈ irreducibleComponents α<GOAL>∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la lb : β<VAR>hab : a ≠ b<VAR>hf : ContinuousOn f (Set.Ioo a b)<VAR>ha : Filter.Tendsto f (𝓝[>] a) (𝓝 la)<VAR>hb : Filter.Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Icc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>T2Space β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>ha : Filter.Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>extendFrom (Set.Ioo a b) f a = la
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>T2Space β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hb : Filter.Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>extendFrom (Set.Ioo a b) f b = lb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>la : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Set.Ioo a b)<VAR>ha : Filter.Tendsto f (𝓝[>] a) (𝓝 la)<GOAL>ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Ico a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>LinearOrder α<VAR>DenselyOrdered α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>RegularSpace β<VAR>f : α → β<VAR>a b : α<VAR>lb : β<VAR>hab : a < b<VAR>hf : ContinuousOn f (Set.Ioo a b)<VAR>hb : Filter.Tendsto f (𝓝[<] b) (𝓝 lb)<GOAL>ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>self : DenseInducing i<GOAL>DenseRange i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>a : α<GOAL>𝓝 a = Filter.comap i (𝓝 (i a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<GOAL>Continuous i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<GOAL>closure (Set.range i) = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>PreconnectedSpace α<VAR>di : DenseInducing i<GOAL>PreconnectedSpace β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>s : Set α<VAR>a : α<VAR>di : DenseInducing i<VAR>hs : s ∈ 𝓝 a<GOAL>closure (i '' s) ∈ 𝓝 (i a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>s : Set α<GOAL>Dense (i '' s) ↔ Dense s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>T2Space β<VAR>di : DenseInducing i<VAR>hd : Dense (Set.range i)ᶜ<VAR>s : Set α<VAR>hs : IsCompact s<GOAL>interior 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>e₁ : α → β<VAR>e₂ : γ → δ<VAR>de₁ : DenseInducing e₁<VAR>de₂ : DenseInducing e₂<GOAL>DenseInducing fun p => (e₁ p.1, e₂ p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>TopologicalSpace.SeparableSpace α<GOAL>TopologicalSpace.SeparableSpace β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>TopologicalSpace δ<VAR>f : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>d : δ<VAR>a : α<VAR>di : DenseInducing i<VAR>H : Filter.Tendsto h (𝓝 d) (𝓝 (i a))<VAR>comm : h ∘ g = i ∘ f<GOAL>Filter.Tendsto f (Filter.comap g (𝓝 d)) (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>b : β<GOAL>(𝓝[Set.range i] b).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>b : β<GOAL>(Filter.comap i (𝓝 b)).NeBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>b : β<VAR>c : γ<VAR>f : α → γ<VAR>hf : Filter.Tendsto f (Filter.comap i (𝓝 b)) (𝓝 c)<GOAL>di.extend f b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → γ<VAR>a : α<VAR>hf : ContinuousAt f a<GOAL>di.extend f (i a) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → γ<VAR>a : α<VAR>c : γ<VAR>hf : Filter.Tendsto f (𝓝 a) (𝓝 c)<GOAL>di.extend f (i a) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>di : DenseInducing i<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → γ<VAR>hf : Continuous f<VAR>a : α<GOAL>di.extend f (i a) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (𝓝 b)) (𝓝 c)<VAR>a : α<GOAL>di.extend f (i a) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>b : β<VAR>f : α → γ<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : α) in Filter.comap i (𝓝 b), g (i x) = f x<VAR>hg : ContinuousAt g b<GOAL>di.extend f b = g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → γ<VAR>g : β → γ<VAR>di : DenseInducing i<VAR>hf : ∀ (x : α), g (i x) = f x<VAR>hg : Continuous g<GOAL>di.extend f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>TopologicalSpace γ<VAR>T3Space γ<VAR>b : β<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Filter.Tendsto f (Filter.comap i (𝓝 x)) (𝓝 c)<GOAL>ContinuousAt (di.extend f) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>TopologicalSpace γ<VAR>T3Space γ<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (𝓝 b)) (𝓝 c)<GOAL>Continuous (di.extend f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>i : α → β<VAR>c : Continuous i<VAR>dense : ∀ (x : β), x ∈ closure (Set.range i)<VAR>H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (i a), ∀ (b : α), i b ∈ t → b ∈ s<GOAL>DenseInducing i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>self : DenseEmbedding e<GOAL>Function.Injective e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>c : Continuous e<VAR>dense : DenseRange e<VAR>inj : Function.Injective e<VAR>H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ (b : α), e b ∈ t → b ∈ s<GOAL>DenseEmbedding e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>de : DenseEmbedding e<VAR>x y : α<GOAL>e x = e y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>de : DenseEmbedding e<GOAL>Embedding e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>de : DenseEmbedding e<VAR>TopologicalSpace.SeparableSpace α<GOAL>TopologicalSpace.SeparableSpace β
<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>e₁ : α → β<VAR>e₂ : γ → δ<VAR>de₁ : DenseEmbedding e₁<VAR>de₂ : DenseEmbedding e₂<GOAL>DenseEmbedding fun p => (e₁ p.1, e₂ p.2)
<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>α : Type u_5<VAR>p : α → Prop<VAR>e : α → β<VAR>x : { x // p x }<GOAL>↑(DenseEmbedding.subtypeEmb p e x) = e ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>de : DenseEmbedding e<VAR>p : α → Prop<GOAL>DenseEmbedding (DenseEmbedding.subtypeEmb p e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>e : α → β<VAR>de : DenseEmbedding e<VAR>s : Set α<GOAL>Dense (e '' s) ↔ Dense s
<VAR>α : Type u_5<VAR>TopologicalSpace α<GOAL>DenseEmbedding id
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>hs : Dense s<GOAL>DenseEmbedding Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>e : α → β<VAR>p : β → Prop<VAR>he : DenseRange e<VAR>hp : IsClosed {x | p x}<VAR>h : ∀ (a : α), p (e a)<VAR>b : β<GOAL>p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>e : α → β<VAR>p : β → β → Prop<VAR>he : DenseRange e<VAR>hp : IsClosed {q | p q.1 q.2}<VAR>h : ∀ (a₁ a₂ : α), p (e a₁) (e a₂)<VAR>b₁ b₂ : β<GOAL>p b₁ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>e : α → β<VAR>p : β → β → β → Prop<VAR>he : DenseRange e<VAR>hp : IsClosed {q | p q.1 q.2.1 q.2.2}<VAR>h : ∀ (a₁ a₂ a₃ : α), p (e a₁) (e a₂) (e a₃)<VAR>b₁ b₂ b₃ : β<GOAL>p b₁ b₂ b₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>e : α → β<VAR>he : DenseRange e<VAR>p : β → Prop<VAR>b₀ : β<VAR>hp : IsClosed {b | p b}<VAR>ih : ∀ (a : α), p (e a)<GOAL>p b₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>T2Space γ<VAR>f : α → β<VAR>hfd : DenseRange f<VAR>g h : β → γ<VAR>hg : Continuous g<VAR>hh : Continuous h<VAR>H : g ∘ f = h ∘ f<GOAL>g = h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>T3Space β<VAR>ι : Type u_5<VAR>s : ι → Set α<VAR>p : ι → Prop<VAR>x : α<VAR>h : (𝓝 x).HasBasis p s<VAR>f : α → β<VAR>hf : DenseInducing f<GOAL>(𝓝 (f x)).HasBasis p fun i => closure (f '' s i)
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>Inf L<VAR>self : ContinuousInf L<GOAL>Continuous fun p => p.1 ⊓ p.2
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>Sup L<VAR>self : ContinuousSup L<GOAL>Continuous fun p => p.1 ⊔ p.2
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>Inf L<VAR>ContinuousInf L<GOAL>Continuous fun p => p.1 ⊓ p.2
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x ⊓ g x
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>Sup L<VAR>ContinuousSup L<GOAL>Continuous fun p => p.1 ⊔ p.2
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => f x ⊔ g x
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>α : Type u_3<VAR>l : Filter α<VAR>f g : α → L<VAR>x y : L<VAR>Sup L<VAR>ContinuousSup L<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (f ⊔ g) l (𝓝 (x ⊔ y))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>α : Type u_3<VAR>l : Filter α<VAR>f g : α → L<VAR>x y : L<VAR>Sup L<VAR>ContinuousSup L<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (fun i => f i ⊔ g i) l (𝓝 (x ⊔ y))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>α : Type u_3<VAR>l : Filter α<VAR>f g : α → L<VAR>x y : L<VAR>Inf L<VAR>ContinuousInf L<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (f ⊓ g) l (𝓝 (x ⊓ y))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>α : Type u_3<VAR>l : Filter α<VAR>f g : α → L<VAR>x y : L<VAR>Inf L<VAR>ContinuousInf L<VAR>hf : Filter.Tendsto f l (𝓝 x)<VAR>hg : Filter.Tendsto g l (𝓝 y)<GOAL>Filter.Tendsto (fun i => f i ⊓ g i) l (𝓝 (x ⊓ y))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeSup L<VAR>ContinuousSup L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (s.sup' hne f) l (𝓝 (s.sup' hne g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeSup L<VAR>ContinuousSup L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (fun a => s.sup' hne fun x => f x a) l (𝓝 (s.sup' hne g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (s.inf' hne f) l (𝓝 (s.inf' hne g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeInf L<VAR>ContinuousInf L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (fun a => s.inf' hne fun x => f x a) l (𝓝 (s.inf' hne g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (s.sup f) l (𝓝 (s.sup g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (fun a => s.sup fun x => f x a) l (𝓝 (s.sup g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (s.inf f) l (𝓝 (s.inf g))
<VAR>L : Type u_1<VAR>TopologicalSpace L<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>SemilatticeInf L<VAR>OrderTop L<VAR>ContinuousInf L<VAR>hs : ∀ i ∈ s, Filter.Tendsto (f i) l (𝓝 (g i))<GOAL>Filter.Tendsto (fun a => s.inf fun x => f x a) l (𝓝 (s.inf g))
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (f ⊔ g) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun a => f a ⊔ g a) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (f ⊔ g) s x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun a => f a ⊔ g a) s x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (f ⊔ g) s
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun a => f a ⊔ g a) s
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Sup L<VAR>ContinuousSup L<VAR>f g : X → L<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (f ⊔ g)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (f ⊓ g) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>x : X<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>ContinuousAt (fun a => f a ⊓ g a) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (f ⊓ g) s x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>s : Set X<VAR>x : X<VAR>hf : ContinuousWithinAt f s x<VAR>hg : ContinuousWithinAt g s x<GOAL>ContinuousWithinAt (fun a => f a ⊓ g a) s x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (f ⊓ g) s
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun a => f a ⊓ g a) s
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>Inf L<VAR>ContinuousInf L<VAR>f g : X → L<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous (f ⊓ g)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>ContinuousSup 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.sup' 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>SemilatticeSup L<VAR>ContinuousSup 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.sup' hne f) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>ContinuousSup 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.sup' 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>SemilatticeSup L<VAR>ContinuousSup 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.sup' 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>SemilatticeSup L<VAR>ContinuousSup 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.sup' 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>SemilatticeSup L<VAR>ContinuousSup 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.sup' hne f) t
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous fun a => s.sup' 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>SemilatticeSup L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous (s.sup' hne f)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (fun a => s.sup 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>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.sup f) x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup 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.sup 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>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup 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.sup f) t x
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup 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.sup 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>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>hs : ∀ i ∈ s, ContinuousOn (f i) t<GOAL>ContinuousOn (s.sup f) t
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>TopologicalSpace L<VAR>TopologicalSpace X<VAR>ι : Type u_3<VAR>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous fun a => s.sup 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>SemilatticeSup L<VAR>OrderBot L<VAR>ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>hs : ∀ i ∈ s, Continuous (f i)<GOAL>Continuous (s.sup f)