ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>ι : Type u_5<VAR>TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>y : α<VAR>x : ι<VAR>hf : UpperSemicontinuousAt f y<VAR>hg : ContinuousAt g x<VAR>hy : g x = y<GOAL>UpperSemicontinuousAt (fun x => f (g x)) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>Preorder β<VAR>ι : Type u_5<VAR>TopologicalSpace ι<VAR>f : α → β<VAR>g : ι → α<VAR>hf : UpperSemicontinuous f<VAR>hg : Continuous g<GOAL>UpperSemicontinuous fun x => f (g x)
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousWithinAt f s x<VAR>hg : UpperSemicontinuousWithinAt g s x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>UpperSemicontinuousWithinAt (fun z => f z + g z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousAt f x<VAR>hg : UpperSemicontinuousAt g x<VAR>hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>UpperSemicontinuousAt (fun z => f z + g z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousOn f s<VAR>hg : UpperSemicontinuousOn g s<VAR>hcont : ∀ x ∈ s, ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>UpperSemicontinuousOn (fun z => f z + g z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuous f<VAR>hg : UpperSemicontinuous g<VAR>hcont : ∀ (x : α), ContinuousAt (fun p => p.1 + p.2) (f x, g x)<GOAL>UpperSemicontinuous fun z => f z + g z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousWithinAt f s x<VAR>hg : UpperSemicontinuousWithinAt g s x<GOAL>UpperSemicontinuousWithinAt (fun z => f z + g z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousAt f x<VAR>hg : UpperSemicontinuousAt g x<GOAL>UpperSemicontinuousAt (fun z => f z + g z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuousOn f s<VAR>hg : UpperSemicontinuousOn g s<GOAL>UpperSemicontinuousOn (fun z => f z + g z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f g : α → γ<VAR>hf : UpperSemicontinuous f<VAR>hg : UpperSemicontinuous g<GOAL>UpperSemicontinuous fun z => f z + g z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, UpperSemicontinuousWithinAt (f i) s x<GOAL>UpperSemicontinuousWithinAt (fun z => ∑ i ∈ a, f i z) s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, UpperSemicontinuousAt (f i) x<GOAL>UpperSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, UpperSemicontinuousOn (f i) s<GOAL>UpperSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Type u_3<VAR>γ : Type u_4<VAR>LinearOrderedAddCommMonoid γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>ContinuousAdd γ<VAR>f : ι → α → γ<VAR>a : Finset ι<VAR>ha : ∀ i ∈ a, UpperSemicontinuous (f i)<GOAL>UpperSemicontinuous fun z => ∑ i ∈ a, f i z
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝[s] x, BddBelow (Set.range fun i => f i y)<VAR>h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x<GOAL>UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), UpperSemicontinuousWithinAt (f i) s x<GOAL>UpperSemicontinuousWithinAt (fun x' => ⨅ i, f i x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), UpperSemicontinuousWithinAt (f i hi) s x<GOAL>UpperSemicontinuousWithinAt (fun x' => ⨅ i, ⨅ (hi : p i), f i hi x') s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ᶠ (y : α) in 𝓝 x, BddBelow (Set.range fun i => f i y)<VAR>h : ∀ (i : ι), UpperSemicontinuousAt (f i) x<GOAL>UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), UpperSemicontinuousAt (f i) x<GOAL>UpperSemicontinuousAt (fun x' => ⨅ i, f i x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x<GOAL>UpperSemicontinuousAt (fun x' => ⨅ i, ⨅ (hi : p i), f i hi x') x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ x ∈ s, BddBelow (Set.range fun i => f i x)<VAR>h : ∀ (i : ι), UpperSemicontinuousOn (f i) s<GOAL>UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), UpperSemicontinuousOn (f i) s<GOAL>UpperSemicontinuousOn (fun x' => ⨅ i, f i x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), UpperSemicontinuousOn (f i hi) s<GOAL>UpperSemicontinuousOn (fun x' => ⨅ i, ⨅ (hi : p i), f i hi x') s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>δ' : Type u_5<VAR>ConditionallyCompleteLinearOrder δ'<VAR>f : ι → α → δ'<VAR>bdd : ∀ (x : α), BddBelow (Set.range fun i => f i x)<VAR>h : ∀ (i : ι), UpperSemicontinuous (f i)<GOAL>UpperSemicontinuous fun x' => ⨅ i, f i x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>f : ι → α → δ<VAR>h : ∀ (i : ι), UpperSemicontinuous (f i)<GOAL>UpperSemicontinuous fun x' => ⨅ i, f i x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>ι : Sort u_3<VAR>δ : Type u_4<VAR>CompleteLinearOrder δ<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α → δ<VAR>h : ∀ (i : ι) (hi : p i), UpperSemicontinuous (f i hi)<GOAL>UpperSemicontinuous fun x' => ⨅ i, ⨅ (hi : p i), f i hi x'
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<GOAL>ContinuousWithinAt f s x ↔ LowerSemicontinuousWithinAt f s x ∧ UpperSemicontinuousWithinAt f s x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>x : α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<GOAL>ContinuousAt f x ↔ LowerSemicontinuousAt f x ∧ UpperSemicontinuousAt f x
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>s : Set α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<GOAL>ContinuousOn f s ↔ LowerSemicontinuousOn f s ∧ UpperSemicontinuousOn f s
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>γ : Type u_3<VAR>LinearOrder γ<VAR>TopologicalSpace γ<VAR>OrderTopology γ<VAR>f : α → γ<GOAL>Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>TopologicalSpace.SeparableSpace X<VAR>NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>DiscreteTopology ↑s<GOAL>#↑s < 𝔠
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>TopologicalSpace.SeparableSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>DiscreteTopology ↑s<VAR>hmk : 𝔠 ≤ #↑s<GOAL>¬NormalSpace X
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PartialOrder R<VAR>NonUnitalRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>TopologicalSpace R<VAR>ContinuousStar R<VAR>TopologicalRing R<VAR>sqrt : R → R<VAR>h_continuousOn : ContinuousOn sqrt {x | 0 ≤ x}<VAR>h_sqrt : ∀ (x : R), 0 ≤ x → star (sqrt x) * sqrt x = x<GOAL>StarOrderedRing C(α, R)
<VAR>X : Type u_5<VAR>t : TopologicalSpace X<VAR>self : TopologicalSpace.PseudoMetrizableSpace X<GOAL>∃ m, UniformSpace.toTopologicalSpace = t
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace.PseudoMetrizableSpace Y<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>TopologicalSpace.PseudoMetrizableSpace X
<VAR>X : Type u_5<VAR>t : TopologicalSpace X<VAR>self : TopologicalSpace.MetrizableSpace X<GOAL>∃ m, UniformSpace.toTopologicalSpace = t
<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace.MetrizableSpace Y<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>TopologicalSpace.MetrizableSpace X
<VAR>X : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace.PseudoMetrizableSpace X<VAR>s : Set X<VAR>hs : TopologicalSpace.IsSeparable s<GOAL>SecondCountableTopology ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>⇑(ContinuousMap.equivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>⇑(ContinuousMap.equivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>UniformInducing ⇑(ContinuousMap.equivBoundedOfCompact α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>UniformEmbedding ⇑(ContinuousMap.equivBoundedOfCompact α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>AddMonoid β<VAR>LipschitzAdd β<GOAL>⇑(ContinuousMap.addEquivBoundedOfCompact α β).symm = ⇑(BoundedContinuousFunction.toContinuousMapAddHom α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>AddMonoid β<VAR>LipschitzAdd β<GOAL>⇑(ContinuousMap.addEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>⇑(ContinuousMap.isometryEquivBoundedOfCompact α β).symm = BoundedContinuousFunction.toContinuousMap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>(ContinuousMap.isometryEquivBoundedOfCompact α β).toEquiv = ContinuousMap.equivBoundedOfCompact α β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<GOAL>⇑(ContinuousMap.isometryEquivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<GOAL>dist (BoundedContinuousFunction.mkOfCompact f) (BoundedContinuousFunction.mkOfCompact g) = dist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : α →ᵇ β<GOAL>dist f.toContinuousMap g.toContinuousMap = dist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<VAR>x : α<GOAL>dist (f x) (g x) ≤ dist f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>C0 : 0 ≤ C<GOAL>dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>Nonempty α<GOAL>dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>Nonempty α<GOAL>dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>Nonempty α<VAR>w : ∀ (x : α), dist (f x) (g x) < C<GOAL>dist f g < C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f g : C(α, β)<VAR>C : ℝ<VAR>C0 : 0 < C<GOAL>dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<GOAL>‖BoundedContinuousFunction.mkOfCompact f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : α →ᵇ E<GOAL>‖f.toContinuousMap‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>x : α<GOAL>‖f x‖ ≤ ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>x y : α<GOAL>dist (f x) (f y) ≤ 2 * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>C : ℝ<VAR>C0 : 0 ≤ C<GOAL>‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>Nonempty α<VAR>M : ℝ<GOAL>‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>M : ℝ<VAR>M0 : 0 < M<GOAL>‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>M : ℝ≥0<VAR>M0 : 0 < M<GOAL>‖f‖₊ < M ↔ ∀ (x : α), ‖f x‖₊ < M
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>Nonempty α<VAR>M : ℝ<GOAL>‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<VAR>Nonempty α<VAR>M : ℝ≥0<GOAL>‖f‖₊ < M ↔ ∀ (x : α), ‖f x‖₊ < M
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>f : C(α, ℝ)<VAR>x : α<GOAL>f x ≤ ‖f‖
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>f : C(α, ℝ)<VAR>x : α<GOAL>-‖f‖ ≤ f x
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>f : C(α, E)<GOAL>‖f‖ = ⨆ x, ‖f x‖
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>X : Type u_4<VAR>TopologicalSpace X<VAR>f : C(X, E)<VAR>K L : TopologicalSpace.Compacts X<VAR>hKL : K ≤ L<GOAL>‖ContinuousMap.restrict (↑K) f‖ ≤ ‖ContinuousMap.restrict (↑L) f‖
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_4<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : α →ᵇ E<GOAL>(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).symm f = f.toContinuousMap
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_4<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>f : C(α, E)<VAR>a : α<GOAL>((ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜) f) a = f a
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_4<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toIsometryEquiv = ContinuousMap.isometryEquivBoundedOfCompact α E
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_4<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>↑(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv = ContinuousMap.addEquivBoundedOfCompact α E
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>NormedAddCommGroup E<VAR>𝕜 : Type u_4<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 E<GOAL>(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toEquiv = ContinuousMap.equivBoundedOfCompact α E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MetricSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f : C(α, β)<VAR>ε : ℝ<VAR>h : 0 < ε<GOAL>∃ δ > 0, ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MetricSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f : C(α, β)<VAR>ε : ℝ<VAR>h : 0 < ε<GOAL>0 < f.modulus ε h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>MetricSpace α<VAR>CompactSpace α<VAR>MetricSpace β<VAR>f : C(α, β)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>a b : α<VAR>w : dist a b < f.modulus ε h<GOAL>dist (f a) (f b) < ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup β<VAR>NormedSpace 𝕜 β<VAR>NormedAddCommGroup γ<VAR>NormedSpace 𝕜 γ<VAR>g : β →L[𝕜] γ<GOAL>↑(ContinuousLinearMap.compLeftContinuousCompact X g) = ContinuousLinearMap.compLeftContinuous 𝕜 X g
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup β<VAR>NormedSpace 𝕜 β<VAR>NormedAddCommGroup γ<VAR>NormedSpace 𝕜 γ<VAR>g : β →L[𝕜] γ<VAR>f : C(X, β)<VAR>x : X<GOAL>((ContinuousLinearMap.compLeftContinuousCompact X g) f) x = g (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>T : Type u_3<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<VAR>MetricSpace T<VAR>f : C(X, Y)<VAR>g : C(Y, T)<GOAL>(ContinuousMap.compRightContinuousMap T f) g = g.comp f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>TopologicalSpace X<VAR>CompactSpace X<VAR>TopologicalSpace Y<VAR>CompactSpace Y<VAR>CommSemiring R<VAR>Semiring A<VAR>MetricSpace A<VAR>TopologicalSemiring A<VAR>Algebra R A<VAR>f : C(X, Y)<GOAL>Continuous ⇑(ContinuousMap.compRightAlgHom R A f)
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>LocallyCompactSpace X<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>CompleteSpace E<VAR>ι : Type u_3<VAR>F : ι → C(X, E)<VAR>hF : ∀ (K : TopologicalSpace.Compacts X), Summable fun i => ‖ContinuousMap.restrict (↑K) (F i)‖<GOAL>Summable F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>NormedAddCommGroup β<VAR>StarAddMonoid β<VAR>NormedStarGroup β<VAR>CompactSpace α<VAR>f : C(α, β)<GOAL>BoundedContinuousFunction.mkOfCompact (star f) = star (BoundedContinuousFunction.mkOfCompact f)
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : R[X]<VAR>x : R<GOAL>p.toContinuousMap x = Polynomial.eval x p
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<GOAL>Polynomial.X.toContinuousMap = ContinuousMap.id R
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : R[X]<VAR>X : Set R<VAR>x : ↑X<GOAL>(p.toContinuousMapOn X) x = p.toContinuousMap ↑x
<VAR>R : Type u_1<VAR>Semiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>s : Set R<GOAL>Polynomial.X.toContinuousMapOn s = ContinuousMap.restrict s (ContinuousMap.id R)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>g : R[X]<VAR>f : C(α, R)<VAR>x : α<GOAL>((Polynomial.aeval f) g) x = Polynomial.eval (f x) g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>p : R[X]<GOAL>Polynomial.toContinuousMapAlgHom p = p.toContinuousMap
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>X : Set R<VAR>p : R[X]<GOAL>(Polynomial.toContinuousMapOnAlgHom X) p = p.toContinuousMapOn X
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>X : Set R<GOAL>↑(polynomialFunctions X) = Set.range ⇑(Polynomial.toContinuousMapOnAlgHom X)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>X : Set R<GOAL>(polynomialFunctions X).SeparatesPoints
<VAR>a b : ℝ<VAR>h : a < b<GOAL>Subalgebra.comap (ContinuousMap.compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm.toContinuousMap) (polynomialFunctions unitInterval) = polynomialFunctions (Set.Icc a b)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>s : Set R<GOAL>polynomialFunctions s = Algebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>A : Type u_2<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set R<VAR>φ ψ : C(↑s, R) →ₐ[R] A<VAR>h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)<GOAL>polynomialFunctions s ≤ AlgHom.equalizer φ ψ
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>StarRing R<VAR>ContinuousStar R<VAR>s : Set R<GOAL>(polynomialFunctions s).starClosure = StarAlgebra.adjoin R {(Polynomial.toContinuousMapOnAlgHom s) Polynomial.X}
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>TopologicalSpace R<VAR>TopologicalSemiring R<VAR>A : Type u_2<VAR>StarRing R<VAR>ContinuousStar R<VAR>Semiring A<VAR>StarRing A<VAR>Algebra R A<VAR>s : Set R<VAR>φ ψ : C(↑s, R) →⋆ₐ[R] A<VAR>h : φ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X) = ψ ((Polynomial.toContinuousMapOnAlgHom s) Polynomial.X)<GOAL>(polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<GOAL>1 ≤ GromovHausdorff.maxVar X Y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>CompactSpace X<VAR>Nonempty X<VAR>MetricSpace Y<VAR>CompactSpace Y<VAR>Nonempty Y<VAR>x y : X ⊕ Y<GOAL>dist x y ≤ ↑(GromovHausdorff.maxVar X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y : X ⊕ Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>f (x, y) = f (y, x)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z : X ⊕ Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>f (x, z) ≤ f (x, y) + f (y, z)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x : X ⊕ Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>f (x, x) = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y : X ⊕ Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>0 ≤ f (x, y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<VAR>x y : X<GOAL>f (Sum.inl x, Sum.inl y) = dist x y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<VAR>x y : Y<GOAL>f (Sum.inr x, Sum.inr y) = dist x y
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y : X ⊕ Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<GOAL>f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>MetricSpace X<VAR>MetricSpace Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>fA : f ∈ GromovHausdorff.candidates X Y<VAR>x y : X ⊕ Y<GOAL>f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y) * dist x y