ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>DiscreteTopology δ<VAR>f : α ↪ δ<VAR>g₁ g₂ : BoundedContinuousFunction α β<VAR>h₁ h₂ : BoundedContinuousFunction δ β<GOAL>dist (BoundedContinuousFunction.extend f g₁ h₁) (BoundedContinuousFunction.extend f g₂ h₂) = max (dist g₁ g₂) (dist (h₁.restrict (Set.range ⇑f)ᶜ) (h₂.restrict (Set.range ⇑f)ᶜ))
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>δ : Type u_2<VAR>TopologicalSpace δ<VAR>DiscreteTopology δ<VAR>f : α ↪ δ<VAR>h : BoundedContinuousFunction δ β<GOAL>Isometry fun g => BoundedContinuousFunction.extend f g h
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>PseudoMetricSpace β<VAR>CompactSpace β<VAR>A : Set (BoundedContinuousFunction α β)<VAR>closed : IsClosed A<VAR>H : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact A
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>PseudoMetricSpace β<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (BoundedContinuousFunction α β)<VAR>closed : IsClosed A<VAR>in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact A
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>CompactSpace α<VAR>PseudoMetricSpace β<VAR>T2Space β<VAR>s : Set β<VAR>hs : IsCompact s<VAR>A : Set (BoundedContinuousFunction α β)<VAR>in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s<VAR>H : Equicontinuous fun x => ⇑↑x<GOAL>IsCompact (closure A)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>One β<GOAL>⇑1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<GOAL>⇑0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>CompactSpace α<GOAL>BoundedContinuousFunction.mkOfCompact 0 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>One β<VAR>CompactSpace α<GOAL>BoundedContinuousFunction.mkOfCompact 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>f : BoundedContinuousFunction α β<GOAL>(∀ (x : α), f x = 0) ↔ f = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>One β<VAR>f : BoundedContinuousFunction α β<GOAL>(∀ (x : α), f x = 1) ↔ f = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero β<VAR>TopologicalSpace γ<VAR>f : C(γ, α)<GOAL>BoundedContinuousFunction.compContinuous 0 f = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>One β<VAR>TopologicalSpace γ<VAR>f : C(γ, α)<GOAL>BoundedContinuousFunction.compContinuous 1 f = 1
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>f g : BoundedContinuousFunction α β<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>f g : BoundedContinuousFunction α β<VAR>x : α<GOAL>(f + g) x = f x + g x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>CompactSpace α<VAR>f g : C(α, β)<GOAL>BoundedContinuousFunction.mkOfCompact (f + g) = BoundedContinuousFunction.mkOfCompact f + BoundedContinuousFunction.mkOfCompact g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>f g : BoundedContinuousFunction α β<VAR>TopologicalSpace γ<VAR>h : C(γ, α)<GOAL>(g + f).compContinuous h = g.compContinuous h + f.compContinuous h
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>f : BoundedContinuousFunction α β<VAR>n : ℕ<GOAL>⇑(nsmulRec n f) = n • ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>r : ℕ<VAR>f : BoundedContinuousFunction α β<GOAL>⇑(r • f) = r • ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>r : ℕ<VAR>f : BoundedContinuousFunction α β<VAR>v : α<GOAL>(r • f) v = r • f v
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<GOAL>∀ (a : BoundedContinuousFunction α β) (a_1 : α), BoundedContinuousFunction.coeFnAddHom a a_1 = a a_1
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>self : BoundedContinuousFunction α β<GOAL>(BoundedContinuousFunction.toContinuousMapAddHom α β) self = self.toContinuousMap
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddCommMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → BoundedContinuousFunction α β<GOAL>⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>AddCommMonoid β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f : ι → BoundedContinuousFunction α β<VAR>a : α<GOAL>(∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PseudoMetricSpace R<VAR>Sub R<VAR>BoundedSub R<VAR>ContinuousSub R<VAR>f g : BoundedContinuousFunction α R<VAR>x : α<GOAL>(f - g) x = f x - g x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PseudoMetricSpace R<VAR>Sub R<VAR>BoundedSub R<VAR>ContinuousSub R<VAR>f g : BoundedContinuousFunction α R<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>NatCast β<VAR>n : ℕ<VAR>x : α<GOAL>↑n x = ↑n
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>PseudoMetricSpace β<VAR>IntCast β<VAR>m : ℤ<VAR>x : α<GOAL>↑m x = ↑m
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PseudoMetricSpace R<VAR>Mul R<VAR>BoundedMul R<VAR>ContinuousMul R<VAR>f g : BoundedContinuousFunction α R<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PseudoMetricSpace R<VAR>Mul R<VAR>BoundedMul R<VAR>ContinuousMul R<VAR>f g : BoundedContinuousFunction α R<VAR>x : α<GOAL>(f * g) x = f x * g x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PseudoMetricSpace R<VAR>Monoid R<VAR>BoundedMul R<VAR>ContinuousMul R<VAR>n : ℕ<VAR>f : BoundedContinuousFunction α R<GOAL>⇑(f ^ n) = ⇑f ^ n
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>PseudoMetricSpace R<VAR>Monoid R<VAR>BoundedMul R<VAR>ContinuousMul R<VAR>n : ℕ<VAR>f : BoundedContinuousFunction α R<VAR>x : α<GOAL>(f ^ n) x = f x ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>‖f‖ = dist f 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>‖f‖ = sInf {C | 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>h : Nonempty α<GOAL>‖f‖ = sInf {C | ∀ (x : α), ‖f x‖ ≤ C}
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>IsEmpty α<GOAL>‖f‖ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>x : α<GOAL>‖f x‖ ≤ ‖f‖
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<VAR>x : α<GOAL>-‖f‖ ≤ f x
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<VAR>x : α<GOAL>f x ≤ ‖f‖
<VAR>β : Type v<VAR>γ : Type w<VAR>SeminormedAddCommGroup β<VAR>f : γ → β<VAR>C : ℝ<VAR>hC : ∀ (x : γ), ‖f x‖ ≤ C<VAR>x y : γ<GOAL>dist (f x) (f y) ≤ 2 * C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>x y : α<GOAL>dist (f x) (f y) ≤ 2 * ‖f‖
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>C : ℝ<VAR>C0 : 0 ≤ C<GOAL>‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>Nonempty α<VAR>f : BoundedContinuousFunction α β<VAR>M : ℝ<GOAL>‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>CompactSpace α<VAR>f : BoundedContinuousFunction α β<VAR>M : ℝ<VAR>M0 : 0 < M<GOAL>‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>Nonempty α<VAR>CompactSpace α<VAR>f : BoundedContinuousFunction α β<VAR>M : ℝ<GOAL>‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>b : β<GOAL>‖BoundedContinuousFunction.const α b‖ ≤ ‖b‖
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>h : Nonempty α<VAR>b : β<GOAL>‖BoundedContinuousFunction.const α b‖ = ‖b‖
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>Hf : Continuous f<VAR>C : ℝ<VAR>H : ∀ (x : α), ‖f x‖ ≤ C<GOAL>⇑(BoundedContinuousFunction.ofNormedAddCommGroup f Hf C H) = f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>hfc : Continuous f<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>hfC : ∀ (x : α), ‖f x‖ ≤ C<GOAL>‖BoundedContinuousFunction.ofNormedAddCommGroup f hfc C hfC‖ ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>DiscreteTopology α<VAR>SeminormedAddCommGroup β<VAR>f : α → β<VAR>C : ℝ<VAR>H : ∀ (x : α), ‖f x‖ ≤ C<GOAL>⇑(BoundedContinuousFunction.ofNormedAddCommGroupDiscrete f C H) = f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑f.normComp = norm ∘ ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>‖f.normComp‖ = ‖f‖
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>BddAbove (Set.range (norm ∘ ⇑f))
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>‖f‖ = ⨆ x, ‖f x‖
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑(-f) = -⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>x : α<GOAL>(-f) x = -f x
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>CompactSpace α<VAR>f : C(α, β)<GOAL>BoundedContinuousFunction.mkOfCompact (-f) = -BoundedContinuousFunction.mkOfCompact f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>CompactSpace α<VAR>f g : C(α, β)<GOAL>BoundedContinuousFunction.mkOfCompact (f - g) = BoundedContinuousFunction.mkOfCompact f - BoundedContinuousFunction.mkOfCompact g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>z : ℤ<GOAL>⇑(zsmulRec (fun x x_1 => x • x_1) z f) = z • ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>r : ℤ<VAR>f : BoundedContinuousFunction α β<GOAL>⇑(r • f) = r • ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>r : ℤ<VAR>f : BoundedContinuousFunction α β<VAR>v : α<GOAL>(r • f) v = r • f v
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>‖f‖₊ = nndist f 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>x : α<GOAL>‖f x‖₊ ≤ ‖f‖₊
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>x y : α<GOAL>nndist (f x) (f y) ≤ 2 * ‖f‖₊
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<VAR>C : ℝ≥0<GOAL>‖f‖₊ ≤ C ↔ ∀ (x : α), ‖f x‖₊ ≤ C
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>b : β<GOAL>‖BoundedContinuousFunction.const α b‖₊ ≤ ‖b‖₊
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>Nonempty α<VAR>b : β<GOAL>‖BoundedContinuousFunction.const α b‖₊ = ‖b‖₊
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>‖f‖₊ = ⨆ x, ‖f x‖₊
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>f g : BoundedContinuousFunction α β<VAR>x : α<GOAL>‖f x - g x‖ ≤ dist f g
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>x : α<VAR>f g : BoundedContinuousFunction α ℝ<GOAL>f x ≤ g x + dist f g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>TopologicalSpace γ<VAR>f : BoundedContinuousFunction α β<VAR>g : C(γ, α)<GOAL>‖f.compContinuous g‖ ≤ ‖f‖
<VAR>α : Type u<VAR>β : Type v<VAR>𝕜 : Type u_2<VAR>PseudoMetricSpace 𝕜<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero 𝕜<VAR>Zero β<VAR>SMul 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>f : BoundedContinuousFunction α β<GOAL>⇑(c • f) = fun x => c • f x
<VAR>α : Type u<VAR>β : Type v<VAR>𝕜 : Type u_2<VAR>PseudoMetricSpace 𝕜<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Zero 𝕜<VAR>Zero β<VAR>SMul 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>f : BoundedContinuousFunction α β<VAR>x : α<GOAL>(c • f) x = c • f x
<VAR>α : Type u<VAR>β : Type v<VAR>𝕜 : Type u_2<VAR>PseudoMetricSpace 𝕜<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Semiring 𝕜<VAR>AddCommMonoid β<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>x : α<VAR>f : BoundedContinuousFunction α β<GOAL>(BoundedContinuousFunction.evalCLM 𝕜 x) f = f x
<VAR>α : Type u<VAR>β : Type v<VAR>𝕜 : Type u_2<VAR>PseudoMetricSpace 𝕜<VAR>TopologicalSpace α<VAR>PseudoMetricSpace β<VAR>Semiring 𝕜<VAR>AddCommMonoid β<VAR>Module 𝕜 β<VAR>BoundedSMul 𝕜 β<VAR>BoundedAdd β<VAR>ContinuousAdd β<VAR>self : BoundedContinuousFunction α β<GOAL>(BoundedContinuousFunction.toContinuousMapLinearMap α β 𝕜) self = self.toContinuousMap
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>𝕜 : Type u_2<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 β<VAR>SeminormedAddCommGroup γ<VAR>NormedSpace 𝕜 γ<VAR>g : β →L[𝕜] γ<VAR>f : BoundedContinuousFunction α β<VAR>x : α<GOAL>((ContinuousLinearMap.compLeftContinuousBounded α g) f) x = g (f x)
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>SeminormedRing R<VAR>f : BoundedContinuousFunction α R<VAR>n : ℕ<GOAL>⇑(npowRec n f) = ⇑f ^ n
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>SeminormedRing R<VAR>n : ℕ<GOAL>⇑↑n = ↑n
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>SeminormedRing R<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>⇑(OfNat.ofNat n) = OfNat.ofNat n
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>SeminormedRing R<VAR>n : ℤ<GOAL>⇑↑n = ↑n
<VAR>α : Type u<VAR>γ : Type w<VAR>𝕜 : Type u_2<VAR>NormedField 𝕜<VAR>TopologicalSpace α<VAR>NormedRing γ<VAR>NormedAlgebra 𝕜 γ<VAR>k : 𝕜<VAR>a : α<GOAL>((algebraMap 𝕜 (BoundedContinuousFunction α γ)) k) a = k • 1
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ≥0<VAR>x : α<GOAL>f x ≤ nndist f 0
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>StarAddMonoid β<VAR>NormedStarGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑(star f) = star ⇑f
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>SeminormedAddCommGroup β<VAR>StarAddMonoid β<VAR>NormedStarGroup β<VAR>f : BoundedContinuousFunction α β<VAR>x : α<GOAL>(star f) x = star (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>NormedLatticeAddCommGroup β<VAR>f g : BoundedContinuousFunction α β<GOAL>⇑(f ⊔ g) = ⇑f ⊔ ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>NormedLatticeAddCommGroup β<VAR>f g : BoundedContinuousFunction α β<GOAL>⇑(f ⊓ g) = ⇑f ⊓ ⇑g
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>NormedLatticeAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑|f| = |⇑f|
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>NormedLatticeAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑f⁺ = (⇑f)⁺
<VAR>α : Type u<VAR>β : Type v<VAR>TopologicalSpace α<VAR>NormedLatticeAddCommGroup β<VAR>f : BoundedContinuousFunction α β<GOAL>⇑f⁻ = (⇑f)⁻
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<GOAL>⇑f.nnrealPart = Real.toNNReal ∘ ⇑f
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<GOAL>⇑f.nnnorm = nnnorm ∘ ⇑f
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<GOAL>⇑f = NNReal.toReal ∘ ⇑f.nnrealPart - NNReal.toReal ∘ ⇑(-f).nnrealPart
<VAR>α : Type u<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<GOAL>abs ∘ ⇑f = NNReal.toReal ∘ ⇑f.nnrealPart + NNReal.toReal ∘ ⇑(-f).nnrealPart
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<GOAL>0 ≤ f + BoundedContinuousFunction.const α ‖f‖
<VAR>α : Type u_2<VAR>TopologicalSpace α<VAR>f : BoundedContinuousFunction α ℝ<GOAL>0 ≤ BoundedContinuousFunction.const α ‖f‖ - f
<VAR>R : Type u_1<VAR>Field R<VAR>M : Type u_2<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>A : M ≃L[R] M<GOAL>(↑A.symm).det = (↑A).det⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<GOAL>UniformFun.toFun 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<GOAL>UniformFun.toFun 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>One β<GOAL>UniformFun.ofFun 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Zero β<GOAL>UniformFun.ofFun 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>One β<GOAL>(UniformOnFun.toFun 𝔖) 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Zero β<GOAL>(UniformOnFun.toFun 𝔖) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Zero β<GOAL>(UniformOnFun.ofFun 𝔖) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>One β<GOAL>(UniformOnFun.ofFun 𝔖) 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul β<VAR>f g : α →ᵤ β<GOAL>UniformFun.toFun (f * g) = UniformFun.toFun f * UniformFun.toFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>f g : α →ᵤ β<GOAL>UniformFun.toFun (f + g) = UniformFun.toFun f + UniformFun.toFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Mul β<VAR>f g : α → β<GOAL>UniformFun.ofFun (f * g) = UniformFun.ofFun f * UniformFun.ofFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Add β<VAR>f g : α → β<GOAL>UniformFun.ofFun (f + g) = UniformFun.ofFun f + UniformFun.ofFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Add β<VAR>f g : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) (f + g) = (UniformOnFun.toFun 𝔖) f + (UniformOnFun.toFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Mul β<VAR>f g : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) (f * g) = (UniformOnFun.toFun 𝔖) f * (UniformOnFun.toFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Mul β<VAR>f g : α → β<GOAL>(UniformOnFun.ofFun 𝔖) (f * g) = (UniformOnFun.ofFun 𝔖) f * (UniformOnFun.ofFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Add β<VAR>f g : α → β<GOAL>(UniformOnFun.ofFun 𝔖) (f + g) = (UniformOnFun.ofFun 𝔖) f + (UniformOnFun.ofFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Inv β<VAR>f : α →ᵤ β<GOAL>UniformFun.toFun f⁻¹ = (UniformFun.toFun f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Neg β<VAR>f : α →ᵤ β<GOAL>UniformFun.toFun (-f) = -UniformFun.toFun f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Neg β<VAR>f : α → β<GOAL>UniformFun.ofFun (-f) = -UniformFun.ofFun f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Inv β<VAR>f : α → β<GOAL>UniformFun.ofFun f⁻¹ = (UniformFun.ofFun f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Inv β<VAR>f : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) f⁻¹ = ((UniformOnFun.toFun 𝔖) f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Neg β<VAR>f : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) (-f) = -(UniformOnFun.toFun 𝔖) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Neg β<VAR>f : α → β<GOAL>(UniformOnFun.ofFun 𝔖) (-f) = -(UniformOnFun.ofFun 𝔖) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Inv β<VAR>f : α → β<GOAL>(UniformOnFun.ofFun 𝔖) f⁻¹ = ((UniformOnFun.ofFun 𝔖) f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Div β<VAR>f g : α →ᵤ β<GOAL>UniformFun.toFun (f / g) = UniformFun.toFun f / UniformFun.toFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Sub β<VAR>f g : α →ᵤ β<GOAL>UniformFun.toFun (f - g) = UniformFun.toFun f - UniformFun.toFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Div β<VAR>f g : α → β<GOAL>UniformFun.ofFun (f / g) = UniformFun.ofFun f / UniformFun.ofFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Sub β<VAR>f g : α → β<GOAL>UniformFun.ofFun (f - g) = UniformFun.ofFun f - UniformFun.ofFun g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Sub β<VAR>f g : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) (f - g) = (UniformOnFun.toFun 𝔖) f - (UniformOnFun.toFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Div β<VAR>f g : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) (f / g) = (UniformOnFun.toFun 𝔖) f / (UniformOnFun.toFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Sub β<VAR>f g : α → β<GOAL>(UniformOnFun.ofFun 𝔖) (f - g) = (UniformOnFun.ofFun 𝔖) f - (UniformOnFun.ofFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>Div β<VAR>f g : α → β<GOAL>(UniformOnFun.ofFun 𝔖) (f / g) = (UniformOnFun.ofFun 𝔖) f / (UniformOnFun.ofFun 𝔖) g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>SMul M β<VAR>c : M<VAR>f : α →ᵤ β<GOAL>UniformFun.toFun (c • f) = c • UniformFun.toFun f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>SMul M β<VAR>c : M<VAR>f : α → β<GOAL>UniformFun.ofFun (c • f) = c • UniformFun.ofFun f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>M : Type u_5<VAR>SMul M β<VAR>c : M<VAR>f : α →ᵤ[𝔖] β<GOAL>(UniformOnFun.toFun 𝔖) (c • f) = c • (UniformOnFun.toFun 𝔖) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝔖 : Set (Set α)<VAR>M : Type u_5<VAR>SMul M β<VAR>c : M<VAR>f : α → β<GOAL>(UniformOnFun.ofFun 𝔖) (c • f) = c • (UniformOnFun.ofFun 𝔖) f
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>AddGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 0).HasBasis p b<GOAL>(𝓝 0).HasBasis p fun i => {f | ∀ (x : α), UniformFun.toFun f x ∈ b i}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>Group G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<GOAL>(𝓝 1).HasBasis p fun i => {f | ∀ (x : α), UniformFun.toFun f x ∈ b i}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>UniformSpace G<VAR>UniformGroup G<GOAL>(𝓝 1).HasBasis (fun V => V ∈ 𝓝 1) fun V => {f | ∀ (x : α), f x ∈ V}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<GOAL>(𝓝 0).HasBasis (fun V => V ∈ 𝓝 0) fun V => {f | ∀ (x : α), f x ∈ V}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>AddGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 0).HasBasis p b<GOAL>(𝓝 0).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>ι : Type u_3<VAR>Group G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>b : ι → Set G<VAR>h : (𝓝 1).HasBasis p b<GOAL>(𝓝 1).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {f | ∀ x ∈ Si.1, (UniformOnFun.toFun 𝔖) f x ∈ b Si.2}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>Group G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<GOAL>(𝓝 1).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓝 1) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}