ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<GOAL>BddBelow (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>Zero α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactSupport f<GOAL>BddBelow (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>One α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactMulSupport f<GOAL>BddAbove (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>Zero α<VAR>f : β → α<VAR>hf : Continuous f<VAR>h : HasCompactSupport f<GOAL>BddAbove (Set.range f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>h0K : K.Nonempty<VAR>hf : ContinuousOn f K<VAR>y : α<GOAL>sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>h0K : K.Nonempty<VAR>hf : ContinuousOn f K<VAR>y : α<GOAL>y < sInf (f '' K) ↔ ∀ x ∈ K, y < f x
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>sInf s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>sSup s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>IsGLB s (sInf s)
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>IsLUB s (sSup s)
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIicTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>IsLeast s (sInf s)
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>ClosedIciTopology α<VAR>s : Set α<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<GOAL>IsGreatest s (sSup s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, sSup (f '' s) = f x ∧ ∀ y ∈ s, f y ≤ f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<VAR>hf : ContinuousOn f s<GOAL>∃ x ∈ s, sInf (f '' s) = f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>s : Set β<VAR>hs : IsCompact s<VAR>ne_s : s.Nonempty<VAR>f : β → α<GOAL>ContinuousOn f s → ∃ x ∈ s, sSup (f '' s) = f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>s t : Set β<VAR>z : β<VAR>ht : IsCompact t<VAR>hf : ContinuousOn f t<VAR>hz : z ∈ t<VAR>hfz : ∀ z' ∈ t \ s, f z < f z'<GOAL>∃ x ∈ s, IsMinOn f t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>s t : Set β<VAR>z : β<VAR>ht : IsCompact t<VAR>hf : ContinuousOn f t<VAR>hz : z ∈ t<VAR>hfz : ∀ z' ∈ t \ s, f z' < f z<GOAL>∃ x ∈ s, IsMaxOn f t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>s t : Set β<VAR>z : β<VAR>ht : IsCompact t<VAR>hf : ContinuousOn f t<VAR>hz : z ∈ t<VAR>hfz : ∀ z' ∈ t \ s, f z < f z'<GOAL>∃ x ∈ s, IsLocalMinOn f t x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIicTopology α<VAR>f : β → α<VAR>s t : Set β<VAR>z : β<VAR>ht : IsCompact t<VAR>hst : s ⊆ t<VAR>hf : ContinuousOn f t<VAR>hz : z ∈ t<VAR>hfz : ∀ z' ∈ t \ s, f z < f z'<VAR>hs : IsOpen s<GOAL>∃ x ∈ s, IsLocalMin f x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>ClosedIciTopology α<VAR>f : β → α<VAR>s t : Set β<VAR>z : β<VAR>ht : IsCompact t<VAR>hst : s ⊆ t<VAR>hf : ContinuousOn f t<VAR>hz : z ∈ t<VAR>hfz : ∀ z' ∈ t \ s, f z' < f z<VAR>hs : IsOpen s<GOAL>∃ x ∈ s, IsLocalMax f x
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>s : Set α<VAR>h₁ : IsConnected s<VAR>h₂ : IsCompact s<GOAL>s = Set.Icc (sInf s) (sSup s)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<GOAL>Continuous fun x => sSup (f x '' K)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>f : γ → β → α<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hf : Continuous ↿f<GOAL>Continuous fun x => sInf (f x '' K)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>DenselyOrdered α<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTopology β<VAR>f : α → β<VAR>a b : α<VAR>hab : a ≤ b<VAR>h : ContinuousOn f (Set.Icc a b)<GOAL>f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>DenselyOrdered α<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTopology β<VAR>f : α → β<VAR>a b : α<VAR>h : ContinuousOn f (Set.uIcc a b)<GOAL>f '' Set.uIcc a b = Set.Icc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>DenselyOrdered α<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTopology β<VAR>f : α → β<VAR>a b : α<VAR>h : ContinuousOn f (Set.uIcc a b)<GOAL>f '' Set.uIcc a b = Set.uIcc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>DenselyOrdered α<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f (Set.Icc a b)<VAR>hc : c ∈ Set.Icc a b<GOAL>sInf (f '' Set.Icc a b) ≤ f c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ConditionallyCompleteLinearOrder α<VAR>TopologicalSpace α<VAR>OrderTopology α<VAR>TopologicalSpace β<VAR>DenselyOrdered α<VAR>ConditionallyCompleteLinearOrder β<VAR>OrderTopology β<VAR>f : α → β<VAR>a b c : α<VAR>h : ContinuousOn f (Set.Icc a b)<VAR>hc : c ∈ Set.Icc a b<GOAL>f c ≤ sSup (f '' Set.Icc a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Add β<VAR>ContinuousAdd β<VAR>f g : C(α, β)<GOAL>⇑(f + g) = ⇑f + ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Mul β<VAR>ContinuousMul β<VAR>f g : C(α, β)<GOAL>⇑(f * g) = ⇑f * ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Add β<VAR>ContinuousAdd β<VAR>f g : C(α, β)<VAR>x : α<GOAL>(f + g) x = f x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Mul β<VAR>ContinuousMul β<VAR>f g : C(α, β)<VAR>x : α<GOAL>(f * g) x = f x * g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Mul γ<VAR>ContinuousMul γ<VAR>f₁ f₂ : C(β, γ)<VAR>g : C(α, β)<GOAL>(f₁ * f₂).comp g = f₁.comp g * f₂.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Add γ<VAR>ContinuousAdd γ<VAR>f₁ f₂ : C(β, γ)<VAR>g : C(α, β)<GOAL>(f₁ + f₂).comp g = f₁.comp g + f₂.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<GOAL>⇑0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>One β<GOAL>⇑1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Zero β<VAR>x : α<GOAL>0 x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>One β<VAR>x : α<GOAL>1 x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>One γ<VAR>g : C(α, β)<GOAL>ContinuousMap.comp 1 g = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Zero γ<VAR>g : C(α, β)<GOAL>ContinuousMap.comp 0 g = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>NatCast β<VAR>n : ℕ<GOAL>⇑↑n = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>NatCast β<VAR>n : ℕ<VAR>x : α<GOAL>↑n x = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>IntCast β<VAR>n : ℤ<GOAL>⇑↑n = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>IntCast β<VAR>n : ℤ<VAR>x : α<GOAL>↑n x = ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>n : ℕ<VAR>f : C(α, β)<GOAL>⇑(n • f) = n • ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Monoid β<VAR>ContinuousMul β<VAR>f : C(α, β)<VAR>n : ℕ<GOAL>⇑(f ^ n) = ⇑f ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>f : C(α, β)<VAR>n : ℕ<VAR>x : α<GOAL>(n • f) x = n • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Monoid β<VAR>ContinuousMul β<VAR>f : C(α, β)<VAR>n : ℕ<VAR>x : α<GOAL>(f ^ n) x = f x ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>AddMonoid γ<VAR>ContinuousAdd γ<VAR>f : C(β, γ)<VAR>n : ℕ<VAR>g : C(α, β)<GOAL>(n • f).comp g = n • f.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Monoid γ<VAR>ContinuousMul γ<VAR>f : C(β, γ)<VAR>n : ℕ<VAR>g : C(α, β)<GOAL>(f ^ n).comp g = f.comp g ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Neg β<VAR>ContinuousNeg β<VAR>f : C(α, β)<GOAL>⇑(-f) = -⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Inv β<VAR>ContinuousInv β<VAR>f : C(α, β)<GOAL>⇑f⁻¹ = (⇑f)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Neg β<VAR>ContinuousNeg β<VAR>f : C(α, β)<VAR>x : α<GOAL>(-f) x = -f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Inv β<VAR>ContinuousInv β<VAR>f : C(α, β)<VAR>x : α<GOAL>f⁻¹ x = (f x)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Inv γ<VAR>ContinuousInv γ<VAR>f : C(β, γ)<VAR>g : C(α, β)<GOAL>f⁻¹.comp g = (f.comp g)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Neg γ<VAR>ContinuousNeg γ<VAR>f : C(β, γ)<VAR>g : C(α, β)<GOAL>(-f).comp g = -f.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Div β<VAR>ContinuousDiv β<VAR>f g : C(α, β)<GOAL>⇑(f / g) = ⇑f / ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Sub β<VAR>ContinuousSub β<VAR>f g : C(α, β)<GOAL>⇑(f - g) = ⇑f - ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Div β<VAR>ContinuousDiv β<VAR>f g : C(α, β)<VAR>x : α<GOAL>(f / g) x = f x / g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Sub β<VAR>ContinuousSub β<VAR>f g : C(α, β)<VAR>x : α<GOAL>(f - g) x = f x - g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Sub γ<VAR>ContinuousSub γ<VAR>f g : C(β, γ)<VAR>h : C(α, β)<GOAL>(f - g).comp h = f.comp h - g.comp h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Div γ<VAR>ContinuousDiv γ<VAR>f g : C(β, γ)<VAR>h : C(α, β)<GOAL>(f / g).comp h = f.comp h / g.comp h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>z : ℤ<VAR>f : C(α, β)<GOAL>⇑(z • f) = z • ⇑f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Group β<VAR>TopologicalGroup β<VAR>f : C(α, β)<VAR>z : ℤ<GOAL>⇑(f ^ z) = ⇑f ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>f : C(α, β)<VAR>z : ℤ<VAR>x : α<GOAL>(z • f) x = z • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Group β<VAR>TopologicalGroup β<VAR>f : C(α, β)<VAR>z : ℤ<VAR>x : α<GOAL>(f ^ z) x = f x ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>Group γ<VAR>TopologicalGroup γ<VAR>f : C(β, γ)<VAR>z : ℤ<VAR>g : C(α, β)<GOAL>(f ^ z).comp g = f.comp g ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>TopologicalSpace γ<VAR>AddGroup γ<VAR>TopologicalAddGroup γ<VAR>f : C(β, γ)<VAR>z : ℤ<VAR>g : C(α, β)<GOAL>(z • f).comp g = z • f.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Monoid β<VAR>ContinuousMul β<VAR>f : C(α, β)<VAR>a : α<GOAL>ContinuousMap.coeFnMonoidHom f a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>f : C(α, β)<VAR>a : α<GOAL>ContinuousMap.coeFnAddMonoidHom f a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>γ : Type u_3<VAR>Monoid β<VAR>ContinuousMul β<VAR>TopologicalSpace γ<VAR>Monoid γ<VAR>ContinuousMul γ<VAR>g : β →* γ<VAR>hg : Continuous ⇑g<VAR>f : C(α, β)<GOAL>(MonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>γ : Type u_3<VAR>AddMonoid β<VAR>ContinuousAdd β<VAR>TopologicalSpace γ<VAR>AddMonoid γ<VAR>ContinuousAdd γ<VAR>g : β →+ γ<VAR>hg : Continuous ⇑g<VAR>f : C(α, β)<GOAL>(AddMonoidHom.compLeftContinuous α g hg) f = { toFun := ⇑g, continuous_toFun := hg }.comp f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>AddZeroClass γ<VAR>ContinuousAdd γ<VAR>g : C(α, β)<VAR>f : C(β, γ)<GOAL>g.compAddMonoidHom' f = f.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>γ : Type u_3<VAR>TopologicalSpace γ<VAR>MulOneClass γ<VAR>ContinuousMul γ<VAR>g : C(α, β)<VAR>f : C(β, γ)<GOAL>g.compMonoidHom' f = f.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>CommMonoid β<VAR>ContinuousMul β<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → C(α, β)<GOAL>⇑(∏ i ∈ s, f i) = ∏ i ∈ s, ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → C(α, β)<GOAL>⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>CommMonoid β<VAR>ContinuousMul β<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → C(α, β)<VAR>a : α<GOAL>(∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → C(α, β)<VAR>a : α<GOAL>(∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>γ : Type u_3<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>f : γ → C(α, β)<VAR>g : C(α, β)<VAR>hf : HasSum f g<VAR>x : α<GOAL>HasSum (fun i => (f i) x) (g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>γ : Type u_3<VAR>f : γ → C(α, β)<VAR>hf : Summable f<VAR>x : α<GOAL>Summable fun i => (f i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>T2Space β<VAR>AddCommMonoid β<VAR>ContinuousAdd β<VAR>γ : Type u_3<VAR>f : γ → C(α, β)<VAR>hf : Summable f<VAR>x : α<GOAL>∑' (i : γ), (f i) x = (∑' (i : γ), f i) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Semiring β<VAR>TopologicalSemiring β<VAR>TopologicalSpace γ<VAR>Semiring γ<VAR>TopologicalSemiring γ<VAR>g : β →+* γ<VAR>hg : Continuous ⇑g<VAR>f : C(α, β)<GOAL>∀ (a : α), ((RingHom.compLeftContinuous α g hg) f) a = g (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Semiring β<VAR>TopologicalSemiring β<VAR>f : C(α, β)<VAR>a : α<GOAL>ContinuousMap.coeFnRingHom f a = f a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>SMul R M<VAR>ContinuousConstSMul R M<VAR>c : R<VAR>f : C(α, M)<GOAL>⇑(c • f) = c • ⇑f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>VAdd R M<VAR>ContinuousConstVAdd R M<VAR>c : R<VAR>f : C(α, M)<GOAL>⇑(c +ᵥ f) = c +ᵥ ⇑f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>VAdd R M<VAR>ContinuousConstVAdd R M<VAR>c : R<VAR>f : C(α, M)<VAR>a : α<GOAL>(c +ᵥ f) a = c +ᵥ f a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>SMul R M<VAR>ContinuousConstSMul R M<VAR>c : R<VAR>f : C(α, M)<VAR>a : α<GOAL>(c • f) a = c • f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>SMul R M<VAR>ContinuousConstSMul R M<VAR>r : R<VAR>f : C(β, M)<VAR>g : C(α, β)<GOAL>(r • f).comp g = r • f.comp g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>VAdd R M<VAR>ContinuousConstVAdd R M<VAR>r : R<VAR>f : C(β, M)<VAR>g : C(α, β)<GOAL>(r +ᵥ f).comp g = r +ᵥ f.comp g
<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>M₂ : Type u_6<VAR>TopologicalSpace M₂<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>ContinuousAdd M<VAR>Module R M<VAR>ContinuousConstSMul R M<VAR>ContinuousAdd M₂<VAR>Module R M₂<VAR>ContinuousConstSMul R M₂<VAR>α : Type u_7<VAR>TopologicalSpace α<VAR>g : M →L[R] M₂<GOAL>∀ (a : C(α, M)), (ContinuousLinearMap.compLeftContinuous R α g) a = (↑(AddMonoidHom.compLeftContinuous α (↑g).toAddMonoidHom ⋯)).toFun a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_3<VAR>M : Type u_5<VAR>TopologicalSpace M<VAR>Semiring R<VAR>AddCommMonoid M<VAR>ContinuousAdd M<VAR>Module R M<VAR>ContinuousConstSMul R M<GOAL>∀ (a : C(α, M)) (a_1 : α), (ContinuousMap.coeFnLinearMap R) a a_1 = (↑ContinuousMap.coeFnAddMonoidHom).toFun a a_1
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>r : R<VAR>a : α<GOAL>(ContinuousMap.C r) a = (algebraMap R A) r
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>A₂ : Type u_4<VAR>TopologicalSpace A₂<VAR>Semiring A₂<VAR>Algebra R A₂<VAR>TopologicalSemiring A₂<VAR>α : Type u_5<VAR>TopologicalSpace α<VAR>g : A →ₐ[R] A₂<VAR>hg : Continuous ⇑g<VAR>f : C(α, A)<GOAL>∀ (a : α), ((AlgHom.compLeftContinuous R g hg) f) a = g (f a)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>α : Type u_5<VAR>β : Type u_6<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>f : C(α, β)<VAR>g : C(β, A)<GOAL>(ContinuousMap.compRightAlgHom R A f) g = g.comp f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>f : C(α, A)<VAR>a : α<GOAL>(ContinuousMap.coeFnAlgHom R) f a = f a
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<GOAL>Monotone fun s => s.SeparatesPoints
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>R : Type u_2<VAR>CommSemiring R<VAR>A : Type u_3<VAR>TopologicalSpace A<VAR>Semiring A<VAR>Algebra R A<VAR>TopologicalSemiring A<VAR>k : R<VAR>a : α<GOAL>((algebraMap R C(α, A)) k) a = k • 1
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>𝕜 : Type u_5<VAR>TopologicalSpace 𝕜<VAR>Field 𝕜<VAR>TopologicalRing 𝕜<VAR>s : Subalgebra 𝕜 C(α, 𝕜)<VAR>h : s.SeparatesPoints<GOAL>(↑s).SeparatesPointsStrongly
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>Group β<VAR>TopologicalGroup β<VAR>Lattice β<VAR>TopologicalLattice β<VAR>f : C(α, β)<GOAL>⇑(mabs f) = mabs ⇑f
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>Lattice β<VAR>TopologicalLattice β<VAR>f : C(α, β)<GOAL>⇑|f| = |⇑f|
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>AddGroup β<VAR>TopologicalAddGroup β<VAR>Lattice β<VAR>TopologicalLattice β<VAR>f : C(α, β)<VAR>x : α<GOAL>|f| x = |f x|
<VAR>α : Type u_1<VAR>TopologicalSpace α<VAR>β : Type u_2<VAR>TopologicalSpace β<VAR>Group β<VAR>TopologicalGroup β<VAR>Lattice β<VAR>TopologicalLattice β<VAR>f : C(α, β)<VAR>x : α<GOAL>(mabs f) x = mabs (f x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Star β<VAR>ContinuousStar β<VAR>f : C(α, β)<GOAL>⇑(star f) = star ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>Star β<VAR>ContinuousStar β<VAR>f : C(α, β)<VAR>x : α<GOAL>(star f) x = star (f x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>𝕜 : Type u_4<VAR>CommSemiring 𝕜<VAR>A : Type u_5<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>Star A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<VAR>f : C(X, Y)<VAR>g : C(Y, A)<GOAL>(ContinuousMap.compStarAlgHom' 𝕜 A f) g = g.comp f
<VAR>X : Type u_1<VAR>TopologicalSpace X<VAR>𝕜 : Type u_4<VAR>CommSemiring 𝕜<VAR>A : Type u_5<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>Star A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<GOAL>ContinuousMap.compStarAlgHom' 𝕜 A (ContinuousMap.id X) = StarAlgHom.id 𝕜 C(X, A)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>TopologicalSpace X<VAR>TopologicalSpace Y<VAR>TopologicalSpace Z<VAR>𝕜 : Type u_4<VAR>CommSemiring 𝕜<VAR>A : Type u_5<VAR>TopologicalSpace A<VAR>Semiring A<VAR>TopologicalSemiring A<VAR>Star A<VAR>ContinuousStar A<VAR>Algebra 𝕜 A<VAR>g : C(Y, Z)<VAR>f : C(X, Y)<GOAL>ContinuousMap.compStarAlgHom' 𝕜 A (g.comp f) = (ContinuousMap.compStarAlgHom' 𝕜 A f).comp (ContinuousMap.compStarAlgHom' 𝕜 A g)