ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<VAR>r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2<VAR>s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<VAR>r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2<VAR>s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2<VAR>lt_r : levyProkhorovEDist μ ν < r<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<VAR>r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2<VAR>s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2<VAR>lt_r : levyProkhorovEDist μ ν < r<VAR>lt_s : levyProkhorovEDist ν κ < s<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<VAR>r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2<VAR>s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2<VAR>lt_r : levyProkhorovEDist μ ν < r<VAR>lt_s : levyProkhorovEDist ν κ < s<VAR>hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<VAR>r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2<VAR>s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2<VAR>lt_r : levyProkhorovEDist μ ν < r<VAR>lt_s : levyProkhorovEDist ν κ < s<VAR>hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε<VAR>hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal<GOAL>μ B ≤ κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε ∧ κ B ≤ μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) + (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) + ε
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : PseudoEMetricSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ ν κ : Measure Ω<VAR>LPμν_finite : ¬levyProkhorovEDist μ ν = ⊤<VAR>LPνκ_finite : ¬levyProkhorovEDist ν κ = ⊤<VAR>ε : ℝ≥0∞<VAR>B : Set Ω<VAR>ε_pos : 0 < ε<VAR>ε_lt_top : ε < ⊤<VAR>B_mble : MeasurableSet B<VAR>half_ε_pos : 0 < ε / 2<VAR>half_ε_lt_top : ε / 2 < ⊤<VAR>r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2<VAR>s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2<VAR>lt_r : levyProkhorovEDist μ ν < r<VAR>lt_s : levyProkhorovEDist ν κ < s<VAR>hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε<VAR>hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal<GOAL>μ B ≤ κ (thickening (s.toReal + r.toReal) B) + (s + r) ∧ κ B ≤ μ (thickening (s.toReal + r.toReal) B) + (s + r)
<VAR>n k : ℕ<GOAL>(n + k).choose k = (n + 1).ascFactorial k / k !
<VAR>n k : ℕ<GOAL>k ! * (n + k).choose k = k ! * ((n + 1).ascFactorial k / k !)
<VAR>n k : ℕ<GOAL>(n + 1).ascFactorial k = k ! * ((n + 1).ascFactorial k / k !)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : NonAssocSemiring α<VAR>inst✝² : NonAssocSemiring β<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : NonAssocSemiring S<VAR>f : R →+* S<VAR>M : Matrix m n R<VAR>v : n → R<VAR>i : m<GOAL>f ((M *ᵥ v) i) = (M.map ⇑f *ᵥ ⇑f ∘ v) i
<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>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>eLpNorm f ⊤ μ < ⊤
<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>f : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>C : ℝ<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C<GOAL>eLpNormEssSup f μ < ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<GOAL>Presieve.IsSheafFor P S.arrows ↔ Nonempty (IsLimit (Fork.ofι (forkMap P S.arrows) ⋯))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<GOAL>Presieve.IsSheafFor P S.arrows ↔ ∀ (a : Presieve.FamilyOfElements P S.arrows), firstMap P S ((firstObjEqFamily P S.arrows).toEquiv.symm a) = secondMap P S ((firstObjEqFamily P S.arrows).toEquiv.symm a) → ∃! x, forkMap P S.arrows x = (firstObjEqFamily P S.arrows).toEquiv.symm a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<GOAL>Presieve.IsSheafFor P S.arrows ↔ ∀ (a : Presieve.FamilyOfElements P S.arrows), ((firstObjEqFamily P S.arrows).hom ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible → ∃! x, forkMap P S.arrows x = (firstObjEqFamily P S.arrows).toEquiv.symm a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<GOAL>Presieve.IsSheafFor P S.arrows ↔ ∀ (a : Presieve.FamilyOfElements P S.arrows), a.Compatible → ∃! x, forkMap P S.arrows x = (firstObjEqFamily P S.arrows).inv a
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<GOAL>∀ (a : Presieve.FamilyOfElements P S.arrows), a.Compatible → ((∃! t, a.IsAmalgamation t) ↔ ∃! x, forkMap P S.arrows x = (firstObjEqFamily P S.arrows).inv a)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : Presieve.FamilyOfElements P S.arrows<VAR>b✝ : x.Compatible<GOAL>(∃! t, x.IsAmalgamation t) ↔ ∃! x_1, forkMap P S.arrows x_1 = (firstObjEqFamily P S.arrows).inv x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : Presieve.FamilyOfElements P S.arrows<VAR>b✝ : x.Compatible<GOAL>∀ (a : P.obj (op X)), x.IsAmalgamation a ↔ forkMap P S.arrows a = (firstObjEqFamily P S.arrows).inv x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : Presieve.FamilyOfElements P S.arrows<VAR>b✝ : x.Compatible<VAR>t : P.obj (op X)<GOAL>x.IsAmalgamation t ↔ forkMap P S.arrows t = (firstObjEqFamily P S.arrows).inv x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : Presieve.FamilyOfElements P S.arrows<VAR>b✝ : x.Compatible<VAR>t : P.obj (op X)<GOAL>x.IsAmalgamation t ↔ forkMap P S.arrows t = (firstObjEqFamily P S.arrows).toEquiv.symm x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>x : Presieve.FamilyOfElements P S.arrows<VAR>b✝ : x.Compatible<VAR>t : P.obj (op X)<GOAL>x.IsAmalgamation t ↔ (firstObjEqFamily P S.arrows).toEquiv (forkMap P S.arrows t) = x
<VAR>T : ℝ<VAR>hT : 0 < T<VAR>t : ℝ<VAR>μ : autoParam (Measure ℝ) _auto✝<GOAL>IsAddFundamentalDomain (↥(zmultiples T)) (Ioc t (t + T)) μ
<VAR>T : ℝ<VAR>hT : 0 < T<VAR>t : ℝ<VAR>μ : autoParam (Measure ℝ) _auto✝<VAR>x : ℝ<GOAL>∃! g, g +ᵥ x ∈ Ioc t (t + T)
<VAR>T : ℝ<VAR>hT : 0 < T<VAR>t : ℝ<VAR>μ : autoParam (Measure ℝ) _auto✝<VAR>x : ℝ<VAR>this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)<GOAL>∃! g, g +ᵥ x ∈ Ioc t (t + T)
<VAR>T : ℝ<VAR>hT : 0 < T<VAR>t : ℝ<VAR>μ : autoParam (Measure ℝ) _auto✝<VAR>x : ℝ<VAR>this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)<GOAL>∃! x_1, codRestrict (fun n => n • T) ↑(zmultiples T) ⋯ x_1 +ᵥ x ∈ Ioc t (t + T)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>c • sphere x r = sphere (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>0 • sphere x r = sphere (0 • x) (‖0‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>hc : c ≠ 0<GOAL>c • sphere x r = sphere (c • x) (‖c‖ * r)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atTop, p x<GOAL>∀ᶠ (n : ℤ) in atTop, p ↑n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atTop, p x<GOAL>∀ᶠ (n : ℤ) in Filter.comap Int.cast atTop, p ↑n
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A✝ : Rep k G✝<VAR>G : Type u_1<VAR>A : Type u_2<VAR>inst✝² : Monoid G<VAR>inst✝¹ : AddCommGroup A<VAR>inst✝ : MulAction G A<VAR>f : G × G → A<VAR>hf : IsTwoCocycle f<VAR>g : G<GOAL>f (1, g) = f (1, 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>t₁ : TopologicalSpace α<VAR>T : Set (TopologicalSpace β)<GOAL>Continuous f ↔ ∀ t ∈ T, Continuous f
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>a : α<VAR>hs : s✝.Finite<VAR>ht : t.Finite<VAR>s : Finset α<GOAL>s ⊆ ht.toFinset ↔ ↑s ⊆ t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>hausdorffEdist s s = 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<GOAL>∀ i ∈ s, infEdist i s = 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f '' s ≤ᶠ[ae μ] s<VAR>h_fin : μ s ≠ ⊤<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>h_fin : μ s ≠ ⊤<VAR>hs' : s ≤ᶠ[ae μ] f ⁻¹' s<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>l m r : List Char<VAR>x✝ : Substring<VAR>h : ValidFor l m r x✝<VAR>n : Nat<GOAL>x✝.nextn (n + 1) { byteIdx := utf8Len m } = { byteIdx := utf8Len m }
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<VAR>hc : 0 < c<GOAL>a / b ≤ c ↔ a / c ≤ b
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>x : Rˣ<GOAL>(x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>h : Integrable I l f vol<GOAL>HasIntegral I l f vol (integral I l f vol)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>h : Integrable I l f vol<GOAL>HasIntegral I l f vol (Exists.choose h)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>x : P × P × P<VAR>hx12 : x.1 ≠ x.2.1<VAR>hx32 : x.2.2 ≠ x.2.1<VAR>f : P × P × P → V × V := fun y => (y.1 -ᵥ y.2.1, y.2.2 -ᵥ y.2.1)<VAR>hf1 : (f x).1 ≠ 0<VAR>hf2 : (f x).2 ≠ 0<GOAL>ContinuousAt (fun y => ∡ y.1 y.2.1 y.2.2) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h1 : 0 < a<VAR>h2 : a < 1<GOAL>1 < 1 / a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l✝ : List α<VAR>a✝ m a : α<VAR>l : List α<GOAL>[a].maximum = max ↑a [].maximum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l✝ : List α<VAR>a✝ m a : α<VAR>l tl : List α<VAR>hd : α<VAR>ih : (a :: tl).maximum = max (↑a) tl.maximum<GOAL>(a :: (tl ++ [hd])).maximum = max (↑a) (tl ++ [hd]).maximum
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : E → E'<VAR>x : E<GOAL>ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x✝ y : α<VAR>m n : ℕ<VAR>x : α<GOAL>x ∈ ⋃ n, ⋃ (_ : n > 0), ptsOfPeriod f n ↔ x ∈ periodicPts f
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h : IsTopologicalBasis s<GOAL>IsTopologicalBasis (s \ {∅})
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h : IsTopologicalBasis s<GOAL>∀ t₁ ∈ s \ {∅}, ∀ t₂ ∈ s \ {∅}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>h : IsTopologicalBasis s<GOAL>t = generateFrom (s \ {∅})
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>∀ᵐ (x : γ) ∂(κ + η) a, x ∈ (κ.mutuallySingularSetSlice η a)ᶜ → ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>MeasurableSet {x | ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x}
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>Measurable fun b => ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>∀ᵐ (x : γ) ∂(κ + η) a, x ∈ (κ.mutuallySingularSetSlice η a)ᶜ → ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>x : γ<VAR>hx : x ∈ (κ.mutuallySingularSetSlice η a)ᶜ<GOAL>ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>x : γ<VAR>hx : κ.rnDerivAux (κ + η) a x < 1<GOAL>ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>x : γ<VAR>hx : κ.rnDerivAux (κ + η) a x < 1<GOAL>ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) = 0 x
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>x : γ<VAR>hx : κ.rnDerivAux (κ + η) a x < 1<GOAL>1 - κ.rnDerivAux (κ + η) a x ≠ 0
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>h_coe : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<VAR>x : γ<VAR>hx : κ.rnDerivAux (κ + η) a x < 1<GOAL>0 ≤ 1 - κ.rnDerivAux (κ + η) a x