ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Nonempty ι<GOAL>f 0 = 0
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁴ : (i : ι) → Module R (M₁ i)<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Nonempty ι<VAR>i : ι<VAR>h✝ : i ∈ univ<GOAL>f 0 = 0
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>(cauSeqIm f).lim = f.lim.im
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>(cauSeqIm f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).im
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<VAR>hA1 : A.card ≤ 1<VAR>hB1 : B.card ≤ 1<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>hA : A.Nonempty<VAR>hB : B.Nonempty<VAR>hA1 : ∀ {a b : G}, a ∈ A → b ∈ A → a = b<VAR>hB1 : ∀ {a b : G}, a ∈ B → b ∈ B → a = b<GOAL>∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : NormedSpace ℝ V<VAR>inst✝² : StrictConvexSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₁ p₂ p₃ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hp₁ : ¬p₂ = p₁<VAR>hp₃ : ¬p₂ = p₃<VAR>hs : Sbtw ℝ p₁ p₂ p₃<GOAL>dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₁₂.τ₃ ≫ S.v₂₃.τ₃ = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<GOAL>((of R).symm (x • y)).support ⊆ x.support +ᵥ ((of R).symm y).support
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<GOAL>x.support.IsPWO
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<GOAL>((of R).symm y).support.IsPWO
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<GOAL>∀ x_1 ∈ ((of R).symm (x • y)).support, x_1 ∈ {a | (VAddAntidiagonal ?m.199459 ?m.199460 a).Nonempty}
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x✝ : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>x : Γ'<VAR>hx : x ∈ ((of R).symm (x✝ • y)).support<GOAL>x ∈ {a | (VAddAntidiagonal ⋯ ⋯ a).Nonempty}
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x✝ : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>x : Γ'<VAR>hx : x ∉ {a | (VAddAntidiagonal ⋯ ⋯ a).Nonempty}<GOAL>x ∉ ((of R).symm (x✝ • y)).support
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>x✝ : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>x : Γ'<VAR>hx : VAddAntidiagonal ⋯ ⋯ x = ∅<GOAL>x ∉ ((of R).symm (x✝ • y)).support
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup G'<VAR>inst✝⁶ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g✝ : E → F<VAR>f'✝ f₀' f₁' g'✝ e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u✝ : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>u : Multiset ι<VAR>x : ι → 𝔸'<VAR>l : List ι<GOAL>HasStrictFDerivAt (fun x => (Multiset.map x ⟦l⟧).prod) (Multiset.map (fun i => (Multiset.map x (Multiset.erase ⟦l⟧ i)).prod • proj i) ⟦l⟧).sum x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>((toFinsupp s).sum fun x => id) = card s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>ι : Type u_3<VAR>x : X<VAR>F : Filter ι<VAR>u : ι → X<GOAL>MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ (a : ι) in F, u a ∈ s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>ι : Type u_3<VAR>x : X<VAR>F : Filter ι<VAR>u : ι → X<GOAL>(∀ {p : X → Prop}, (∀ᶠ (x : X) in 𝓝 x, p x) → ∃ᶠ (a : ι) in F, p (u a)) ↔ ∀ s ∈ 𝓝 x, ∃ᶠ (a : ι) in F, u a ∈ s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hg : UniformConcaveOn s ψ g<GOAL>UniformConcaveOn s (φ + ψ) (f + g)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConcaveOn s φ f<VAR>hg : UniformConcaveOn s ψ g<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>a • (f + g) x + b • (f + g) y + a * b * (φ + ψ) ‖x - y‖ ≤ (f + g) (a • x + b • y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : ¬MeasurableSet s<VAR>x : G<GOAL>condexpIndL1 hm μ s x = 0
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b b' : β a<GOAL>(insert a b (singleton a b')).entries = (singleton a b).entries
<VAR>a x z✝ z : ℂ<GOAL>0 ≤ z.arg ↔ 0 ≤ z.im
<VAR>a x z : ℂ<GOAL>0 ≤ arg 0 ↔ 0 ≤ im 0
<VAR>a x z✝ z : ℂ<VAR>h₀ : z ≠ 0<GOAL>0 ≤ z.arg ↔ 0 ≤ z.im
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>σ : α → Type u_8<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>(l₁.sigma l₂).length = (map (fun a => (l₂ a).length) l₁).sum
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasProjectiveResolutions C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<GOAL>(projectiveResolutions C).map f ≫ Q.iso.hom = P.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>inst✝ : DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.convs' m = g.convs' n
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.342, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>f ≫ g = 𝟙 X₁ ≫ f ≫ g
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.342, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasBinaryBiproducts C<VAR>X₁ X₂ X₃ : CochainComplex C ℤ<VAR>f : X₁ ⟶ X₂<VAR>g : X₂ ⟶ X₃<GOAL>(f ≫ g) ≫ 𝟙 X₃ = f ≫ g
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<GOAL>↑r < 1 ↔ r < 1
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h : Fintype.card R ≤ 2<GOAL>univ = {0, 1}
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h : Fintype.card R ≤ 2<VAR>h✝ : Subsingleton R<GOAL>univ = {0, 1}
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>inst✝¹ : Fintype R<VAR>inst✝ : DecidableEq R<VAR>h : Fintype.card R ≤ 2<VAR>h✝ : Nontrivial R<GOAL>univ = {0, 1}
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.4270<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>u : U<GOAL>φ.symmetrify.star u = ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.4270<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>u : U<GOAL>⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u = Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<GOAL>Memℒp (fun x => c) ⊤ μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<GOAL>eLpNorm (fun x => c) ⊤ μ < ⊤
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ (closure L).toFun s ↔ ∃ t, Term.realize Subtype.val t = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f✝ : α → β<VAR>f : ℕ → α<GOAL>EventuallyConst f atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f✝ : α → β<VAR>f : ℕ → α<GOAL>(∃ i, ∀ (j : ℕ), i ≤ j → f j = f i) ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f✝ : α → β<VAR>f : ℕ → α<VAR>n : ℕ<VAR>h : ∀ (j : ℕ), n ≤ j → f j = f n<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>f (m + 1) = f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f✝ : α → β<VAR>f : ℕ → α<VAR>n : ℕ<VAR>h : ∀ (m : ℕ), n ≤ m → f (m + 1) = f m<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>f m = f n
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>a : R<VAR>ha : ¬IsUnit a<GOAL>(↑{ toFun := fun a => f (χ a), map_one' := ⋯, map_mul' := ⋯ }).toFun a = 0
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.mulOption y i j⟧ = ⟦y.mulOption x j i⟧
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft j⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧ - ⟦y.moveLeft j * x.moveLeft i⟧
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x * y.moveLeft j⟧ + ⟦x.moveLeft i * y⟧ - ⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x⟧ + ⟦y * x.moveLeft i⟧ - ⟦y.moveLeft j * x.moveLeft i⟧
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x * y.moveLeft j⟧ = ⟦y.moveLeft j * x⟧
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.moveLeft i * y⟧ = ⟦y * x.moveLeft i⟧
<VAR>x y : PGame<VAR>i : x.LeftMoves<VAR>j : y.LeftMoves<GOAL>⟦x.moveLeft i * y.moveLeft j⟧ = ⟦y.moveLeft j * x.moveLeft i⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : OrderedCommSemiring α<VAR>inst✝² : StrictOrderedSemiring β<VAR>inst✝¹ : Algebra α β<VAR>inst✝ : SMulPosStrictMono α β<VAR>a a₁ a₂ : α<VAR>ha : 0 < a<GOAL>0 < (algebraMap α β) a
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_indep : iIndep m κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_indep : iIndep m κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>IsPiSystem (piiUnionInter (fun n => {s | MeasurableSet s}) S)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_indep : iIndep m κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>IsPiSystem (piiUnionInter (fun n => {s | MeasurableSet s}) T)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>inst✝ : IsMarkovKernel κ<VAR>m : ι → MeasurableSpace Ω<VAR>h_le : ∀ (i : ι), m i ≤ _mΩ<VAR>h_indep : iIndep m κ μ<VAR>S T : Set ι<VAR>hST : Disjoint S T<GOAL>IndepSets (piiUnionInter (fun n => {s | MeasurableSet s}) S) (piiUnionInter (fun n => {s | MeasurableSet s}) T) κ μ
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>LipschitzWith μ.mass fun f => μ.testAgainstNN f
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<GOAL>∀ (x y : Ω →ᵇ ℝ≥0), dist (μ.testAgainstNN x) (μ.testAgainstNN y) ≤ ↑μ.mass * dist x y
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f₁ f₂ : Ω →ᵇ ℝ≥0<GOAL>dist (μ.testAgainstNN f₁) (μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f₁ f₂ : Ω →ᵇ ℝ≥0<GOAL>|↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂)| ≤ ↑μ.mass * dist f₁ f₂
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>f₁ f₂ : Ω →ᵇ ℝ≥0<GOAL>-(↑μ.mass * dist f₁ f₂) ≤ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ∧ ↑(μ.testAgainstNN f₁) - ↑(μ.testAgainstNN f₂) ≤ ↑μ.mass * dist f₁ f₂
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>y : ↥M<VAR>n : ℕ<GOAL>mk' S (x ^ n) (y ^ n) = mk' S x y ^ n
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>y : ↥M<VAR>n : ℕ<GOAL>(algebraMap R S) x ^ n = (mk' S x y * (algebraMap R S) ↑y) ^ n
<VAR>x : ℤ[i]<GOAL>↑x.re = (toComplex x).re
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<GOAL>(∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s) ↔ ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r<VAR>s' : Set E<VAR>hs' : s' ∈ p.basisSets<GOAL>Absorbs 𝕜 (id s') s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r<VAR>s' : Set E<VAR>hs'✝ : s' ∈ p.basisSets<VAR>I : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hs' : s' = (I.sup p).ball 0 r<GOAL>Absorbs 𝕜 (id s') s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r<VAR>s' : Set E<VAR>hs'✝ : s' ∈ p.basisSets<VAR>I : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hs' : s' = (I.sup p).ball 0 r<VAR>r' : ℝ<VAR>left✝ : r' > 0<VAR>h' : ∀ x ∈ s, (I.sup p) x < r'<GOAL>Absorbs 𝕜 ((I.sup p).ball 0 r) s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r<VAR>s' : Set E<VAR>hs'✝ : s' ∈ p.basisSets<VAR>I : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hs' : s' = (I.sup p).ball 0 r<VAR>r' : ℝ<VAR>left✝ : r' > 0<VAR>h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'<GOAL>Absorbs 𝕜 ((I.sup p).ball 0 r) s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r<VAR>s' : Set E<VAR>hs'✝ : s' ∈ p.basisSets<VAR>I : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hs' : s' = (I.sup p).ball 0 r<VAR>r' : ℝ<VAR>left✝ : r' > 0<VAR>h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'<GOAL>Absorbs 𝕜 ((I.sup p).ball 0 r) ((I.sup p).ball 0 r')
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>hm : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on s)<VAR>hm : ∀ (i : ι), NullMeasurableSet (s i) μ<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>μ (⋃ i, t ∩ s i) = ∑' (i : ι), μ (t ∩ s i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card : finrank 𝕜 E + 1 ≤ s.card<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i ∈ s, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card : finrank 𝕜 E + 1 ≤ s.card<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>∀ I ⊆ s, I.card ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : ι → Set E<VAR>s : Finset ι<VAR>h_card : finrank 𝕜 E + 1 ≤ s.card<VAR>h_convex : ∀ i ∈ s, Convex 𝕜 (F i)<VAR>h_inter : ∀ I ⊆ s, I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<VAR>I : Finset ι<VAR>hI_ss : I ⊆ s<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<GOAL>(⋂ i ∈ I, F i).Nonempty