ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type w<VAR>A : Set M<VAR>L : Language<VAR>inst✝ : L.Structure M<VAR>α : Type u₁<VAR>β : Type u_1<VAR>B : Set M<VAR>s f g : Set (α → M)<VAR>φ : L[[↑A]].Formula α<VAR>hφ : f = setOf φ.Realize<VAR>θ : L[[↑A]].Formula α<VAR>hθ : g = setOf θ.Realize<VAR>x✝ : α → M<GOAL>x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (φ ⊔ θ).Realize
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Subsingleton R<GOAL>p.natDegree = 0
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>M : T.ModelType<VAR>v : α → ↑M<VAR>xs : Fin n → ↑M<GOAL>(φ ⊔ ψ ⇔ ∼(∼φ ⊓ ∼ψ)).Realize v xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hxs : x ∈ s<GOAL>∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hxs : x ∈ s<VAR>H : ∃ m ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ {y | y ∈ s ∧ x ≤ y}, m ≤ z → z ≤ m<GOAL>∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ : Set α<VAR>inst✝ : Preorder α<VAR>s : Set α<VAR>ih : ∀ c ⊆ s, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub<VAR>x : α<VAR>hxs : x ∈ s<VAR>c : Set α<VAR>hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<GOAL>∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>g : α → E'''<VAR>h : f =O[l] g<GOAL>∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>g : α → E'''<VAR>h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖<GOAL>f =O[l] g
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x✝ : α✝ (last n)<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p✝ : (i : Fin n) → α✝ i.castSucc<VAR>i : Fin n<VAR>y✝ : α✝ i.castSucc<VAR>z : α✝ (last n)<VAR>α : Type u_1<VAR>p : Fin 0 → α<VAR>x : α<VAR>y : Fin (0 + 1)<VAR>this : Subsingleton (Fin (0 + 1))<GOAL>snoc p x y = x
<VAR>a b : ℤ<VAR>h : a < b<GOAL>↑(Ioo a b).card = b - a - 1
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<GOAL>1 * k = k
<VAR>a b : Ordinal.{u_1}<VAR>hba : b ≤ a * ω<GOAL>nfp (fun x => a + x) b = a * ω
<VAR>a b : Ordinal.{u_1}<VAR>hba : b ≤ a * ω<GOAL>a * ω ≤ nfp (fun x => a + x) b
<VAR>a b : Ordinal.{u_1}<VAR>hba : b ≤ a * ω<GOAL>a + a * ω ≤ a * ω
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<GOAL>S.toCycles ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a✝ : α✝<VAR>f g : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>h : ∀ (i j : ι), p i → p j → i = j<VAR>a : α<GOAL>(∏ i : ι, if p i then a else 1) = if ∃ i, p i then a else 1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>inst✝ : IsTrans α r<VAR>a : α<VAR>l : List α<VAR>a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b<VAR>hs : Chain r ↑(a :: l)<VAR>b : α<VAR>hb : b ∈ ↑(a :: l)<VAR>c : α<VAR>hc : c ∈ ↑(a :: l)<GOAL>r b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>inst✝ : IsTrans α r<VAR>a : α<VAR>l : List α<VAR>a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b<VAR>hs : List.Pairwise r (a :: (l ++ [a]))<VAR>b : α<VAR>hb : b ∈ ↑(a :: l)<VAR>c : α<VAR>hc : c ∈ ↑(a :: l)<GOAL>r b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>inst✝ : IsTrans α r<VAR>a : α<VAR>l : List α<VAR>a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b<VAR>b : α<VAR>hb : b ∈ ↑(a :: l)<VAR>c : α<VAR>hc : c ∈ ↑(a :: l)<VAR>hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a<GOAL>r b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Cycle α<VAR>inst✝ : IsTrans α r<VAR>a : α<VAR>l : List α<VAR>a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b<VAR>b c : α<VAR>hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a<VAR>hb : b = a ∨ b ∈ l<VAR>hc : c = a ∨ c ∈ l<GOAL>r b c
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>s : Set Z<VAR>x : Z<VAR>hx : f x ∈ e.source<VAR>h : f ⁻¹' e.source ∈ 𝓝[s] x<GOAL>ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>s : Set Z<VAR>x : Z<VAR>hx : f x ∈ e.source<VAR>h : f ⁻¹' e.source ∈ 𝓝[s] x<VAR>fe_cont : ContinuousWithinAt (↑e ∘ f) s x<GOAL>ContinuousWithinAt f s x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>s : Set Z<VAR>x : Z<VAR>hx : f x ∈ e.source<VAR>h : f ⁻¹' e.source ∈ 𝓝[s] x<VAR>fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x<GOAL>ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>f : Z → X<VAR>s : Set Z<VAR>x : Z<VAR>hx : f x ∈ e.source<VAR>h : f ⁻¹' e.source ∈ 𝓝[s] x<VAR>fe_cont : ContinuousWithinAt (↑e ∘ f) (s ∩ f ⁻¹' e.source) x<VAR>this : ContinuousWithinAt (↑e.symm ∘ ↑e ∘ f) (s ∩ f ⁻¹' e.source) x<GOAL>ContinuousWithinAt f (s ∩ f ⁻¹' e.source) x
<VAR>x✝¹ : Substring<VAR>h✝ : x✝¹.Valid<VAR>x✝ : Nat<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝¹<GOAL>(x✝¹.drop x✝).toString.data = List.drop x✝ x✝¹.toString.data
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>X✝ Y✝ : D ⥤ E<VAR>τ : X✝ ⟶ Y✝<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>X✝.map (F.map f) ≫ τ.app (F.obj Y) = τ.app (F.obj X) ≫ Y✝.map (F.map f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>X✝ Y✝ : D ⥤ E<VAR>τ : X✝ ⟶ Y✝<VAR>X Y : C ⥤ D<VAR>f : X ⟶ Y<VAR>x✝ : C<GOAL>X✝.map (f.app x✝) ≫ τ.app (Y.obj x✝) = τ.app (X.obj x✝) ≫ Y✝.map (f.app x✝)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R (Dual R M)<GOAL>map e.flip p.dualCoannihilator = (map e.symm p).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R (Dual R M)<VAR>this : IsReflexive R N<GOAL>map e.flip p.dualCoannihilator = (map e.symm p).dualAnnihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R (Dual R M)<VAR>this : IsReflexive R N<GOAL>map e.flip.symm (map e.symm p).dualAnnihilator = map e.flip.symm (map e.flip p.dualCoannihilator)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R (Dual R M)<VAR>this : IsReflexive R N<GOAL>(map (↑e ∘ₗ ↑e.symm) p).dualCoannihilator = map (↑e.flip.symm ∘ₗ ↑e.flip) p.dualCoannihilator
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : CompleteSpace E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>hf : IntegrableOn f (Ioi 0) ν<VAR>hg : IntegrableOn g (Ioi 0) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>∫ (x : ℝ) in Ioi 0, ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν ∂μ = (L (∫ (x : ℝ) in Ioi 0, f x ∂ν)) (∫ (x : ℝ) in Ioi 0, g x ∂μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : CompleteSpace E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>hf : Integrable ((Ioi 0).indicator f) ν<VAR>hg : Integrable ((Ioi 0).indicator g) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>∫ (x : ℝ) in Ioi 0, ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν ∂μ = (L (∫ (x : ℝ) in Ioi 0, f x ∂ν)) (∫ (x : ℝ) in Ioi 0, g x ∂μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : CompleteSpace E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>hf : Integrable ((Ioi 0).indicator f) ν<VAR>hg : Integrable ((Ioi 0).indicator g) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<GOAL>∫ (x : ℝ), (Ioi 0).indicator (fun x => ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν) x ∂μ = (L (∫ (x : ℝ), (Ioi 0).indicator f x ∂ν)) (∫ (x : ℝ), (Ioi 0).indicator g x ∂μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup E'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>f✝ f' : G → E<VAR>g✝ g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedSpace ℝ E'<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : CompleteSpace E'<VAR>μ ν : Measure ℝ<VAR>inst✝³ : SFinite μ<VAR>inst✝² : SFinite ν<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : NoAtoms ν<VAR>f : ℝ → E<VAR>g : ℝ → E'<VAR>hf : Integrable ((Ioi 0).indicator f) ν<VAR>hg : Integrable ((Ioi 0).indicator g) μ<VAR>L : E →L[ℝ] E' →L[ℝ] F<VAR>x : ℝ<GOAL>((Ioi 0).indicator fun x => ∫ (t : ℝ) in 0 ..x, (L (f t)) (g (x - t)) ∂ν) = (Ioi 0).indicator f ⋆[L, ν] (Ioi 0).indicator g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>c : E<GOAL>ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>cgf 0 μ t = log (μ Set.univ).toReal
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroupWithZero α<VAR>a b c d : α<VAR>m n : ℕ<VAR>hc : c ≠ 0<GOAL>a / c ≤ b / c ↔ a ≤ b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝² : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝¹ : (i : ι) → Module R (φ i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<GOAL>proj i ∘ₗ stdBasis R φ j = diag j i
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : SemilatticeSup α<VAR>a : α<GOAL>Unbounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : SemilatticeSup α<VAR>a : α<GOAL>Bounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Bounded (fun x x_1 => x < x_1) s
<VAR>xl xr : Type u<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → PGame<VAR>x : PGame := mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x => (f ((equivShrink ι).symm x.fst)).moveRight x.snd<GOAL>BddBelow (Set.range f)
<VAR>xl xr : Type u<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → PGame<VAR>x : PGame := mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x => (f ((equivShrink ι).symm x.fst)).moveRight x.snd<VAR>i : ι<GOAL>x ≤ f i
<VAR>xl xr : Type u<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → PGame<VAR>x : PGame := mk PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x => (f ((equivShrink ι).symm x.fst)).moveRight x.snd<VAR>i : ι<GOAL>(∀ (i_1 : x.LeftMoves), x.moveLeft i_1 ⧏ f ((equivShrink ι).symm ((equivShrink ι) i))) ∧ ∀ (j : (f ((equivShrink ι).symm ((equivShrink ι) i))).RightMoves), x ⧏ (f ((equivShrink ι).symm ((equivShrink ι) i))).moveRight j
<VAR>α β : Frm<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget Frm).obj α<GOAL>({ toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ } ≫ { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : Frm<VAR>e : ↑α ≃o ↑β<VAR>x✝ : (forget Frm).obj β<GOAL>({ toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ } ≫ { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<GOAL>ConvexOn 𝕜 s f ↔ Convex 𝕜 s ∧ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) ≤ a • f x + b • f y
<VAR>α : Type u_1<VAR>inst✝ : SemilatticeSup α<VAR>f : ℕ → α<VAR>n : ℕ<VAR>x✝ : α<GOAL>(partialSups f) n ≤ x✝ ↔ (Finset.range (n + 1)).sup' ⋯ f ≤ x✝
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet (Set.univ ∩ {ω | τ ω = i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>inst✝⁶ : MeasurableSpace ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : BorelSpace ι<VAR>inst✝¹ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝ : MetrizableSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)<VAR>m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace<VAR>s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}<GOAL>StronglyMeasurable fun p => (fun i ω => min i (τ ω)) (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>inst✝⁶ : MeasurableSpace ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : BorelSpace ι<VAR>inst✝¹ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝ : MetrizableSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)<VAR>m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace<VAR>s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}<VAR>hs : MeasurableSet s<GOAL>StronglyMeasurable fun p => (fun i ω => min i (τ ω)) (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>inst✝⁶ : MeasurableSpace ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : BorelSpace ι<VAR>inst✝¹ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝ : MetrizableSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)<VAR>m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace<VAR>s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}<VAR>hs : MeasurableSet s<VAR>h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1<GOAL>StronglyMeasurable fun p => (fun i ω => min i (τ ω)) (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>inst✝⁶ : MeasurableSpace ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : BorelSpace ι<VAR>inst✝¹ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝ : MetrizableSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)<VAR>m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace<VAR>s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}<VAR>hs : MeasurableSet s<VAR>h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1<GOAL>Measurable fun p => (fun i ω => min i (τ ω)) (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>inst✝⁶ : MeasurableSpace ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : BorelSpace ι<VAR>inst✝¹ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝ : MetrizableSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)<VAR>m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace<VAR>s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}<VAR>hs : MeasurableSet s<VAR>h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1<GOAL>Measurable (s.restrict fun p => (fun i ω => min i (τ ω)) (↑p.1) p.2)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁷ : LinearOrder ι<VAR>inst✝⁶ : MeasurableSpace ι<VAR>inst✝⁵ : TopologicalSpace ι<VAR>inst✝⁴ : OrderTopology ι<VAR>inst✝³ : SecondCountableTopology ι<VAR>inst✝² : BorelSpace ι<VAR>inst✝¹ : TopologicalSpace β<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>inst✝ : MetrizableSpace ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>m_prod : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑f i)<VAR>m_set : (t : Set (↑(Set.Iic i) × Ω)) → MeasurableSpace ↑t := fun x => Subtype.instMeasurableSpace<VAR>s : Set (↑(Set.Iic i) × Ω) := {p | τ p.2 ≤ i}<VAR>hs : MeasurableSet s<VAR>h_meas_fst : ∀ (t : Set (↑(Set.Iic i) × Ω)), Measurable fun x => ↑(↑x).1<GOAL>Measurable (sᶜ.restrict fun p => (fun i ω => min i (τ ω)) (↑p.1) p.2)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)<VAR>v : Fin (n + 1) → R<GOAL>(det fun i j => v i ^ ↑j) = ∏ i : Fin (n + 1), ∏ j ∈ Ioi i, (v j - v i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>ih : ∀ (v : Fin n → R), (det fun i j => v i ^ ↑j) = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i)<VAR>v : Fin (n + 1) → R<GOAL>∀ (i j : Fin n.succ), of (fun i j => v i ^ ↑j) i j = of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i) i j + vecCons 0 1 i * of (fun i j => vecCons (v 0 ^ ↑j) (fun i => v i.succ ^ ↑j - v 0 ^ ↑j) i) 0 j