ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<GOAL>∀ b ∈ S, 0 * b ∈ AddSubmonoid.closure ↑S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>R : Type u_4<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : SetLike M R<VAR>inst✝ : MulMemClass M R<VAR>S : M<GOAL>∀ (x y : R), (∀ b ∈ S, x * b ∈ AddSubmonoid.closure ↑S) → (∀ b ∈ S, y * b ∈ AddSubmonoid.closure ↑S) → ∀ b ∈ S, (x + y) * b ∈ AddSubmonoid.closure ↑S
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁶ : Group H<VAR>inst✝⁵ : SMul G α<VAR>inst✝⁴ : SMul G β<VAR>inst✝³ : MulAction H α<VAR>inst✝² : SMul H β<VAR>inst✝¹ : SMulCommClass G H β<VAR>inst✝ : SMulCommClass G H α<VAR>s t : Set α<VAR>b : β<VAR>g : H<VAR>h : Supports G s b<VAR>g' : G<VAR>hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a<GOAL>g' • g • b = g • b
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁶ : Group H<VAR>inst✝⁵ : SMul G α<VAR>inst✝⁴ : SMul G β<VAR>inst✝³ : MulAction H α<VAR>inst✝² : SMul H β<VAR>inst✝¹ : SMulCommClass G H β<VAR>inst✝ : SMulCommClass G H α<VAR>s t : Set α<VAR>b : β<VAR>g : H<VAR>h : Supports G s b<VAR>g' : G<VAR>hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a<GOAL>∀ ⦃a : α⦄, a ∈ s → g' • a = a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁶ : Group H<VAR>inst✝⁵ : SMul G α<VAR>inst✝⁴ : SMul G β<VAR>inst✝³ : MulAction H α<VAR>inst✝² : SMul H β<VAR>inst✝¹ : SMulCommClass G H β<VAR>inst✝ : SMulCommClass G H α<VAR>s t : Set α<VAR>b : β<VAR>g : H<VAR>h : Supports G s b<VAR>g' : G<VAR>hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a<VAR>a : α<VAR>ha : a ∈ s<GOAL>g' • a = a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝⁶ : Group H<VAR>inst✝⁵ : SMul G α<VAR>inst✝⁴ : SMul G β<VAR>inst✝³ : MulAction H α<VAR>inst✝² : SMul H β<VAR>inst✝¹ : SMulCommClass G H β<VAR>inst✝ : SMulCommClass G H α<VAR>s t : Set α<VAR>b : β<VAR>g : H<VAR>h : Supports G s b<VAR>g' : G<VAR>hg' : ∀ ⦃a : α⦄, a ∈ g • s → g' • a = a<VAR>a : α<VAR>ha : a ∈ s<VAR>this : g' • g • a = g • a<GOAL>g' • a = a
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : SemilatticeSup β<VAR>u : β → α<GOAL>Tendsto (fun p => (u p.1, u p.2)) (atTop ×ˢ atTop) (𝓤 α) ↔ Tendsto (Prod.map u u) atTop (𝓤 α)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r✝ : ℝ<VAR>inst✝ : ProperSpace α<VAR>c : α<VAR>r : ℝ<VAR>h : (closedBall c r)ᶜ ⊆ s<GOAL>s ∈ cocompact α
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x : α<VAR>s t : Set α<VAR>r✝ : ℝ<VAR>inst✝ : ProperSpace α<VAR>c : α<VAR>r : ℝ<VAR>h : (closedBall c r)ᶜ ⊆ s<GOAL>∃ t, IsCompact t ∧ tᶜ ⊆ s
<VAR>α β : BddLat<VAR>e : ↑α.toLat ≃o ↑β.toLat<VAR>x✝ : (forget BddLat).obj α<GOAL>((let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : BddLat<VAR>e : ↑α.toLat ≃o ↑β.toLat<VAR>x✝ : (forget BddLat).obj β<GOAL>((let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫ let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ }; { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 β) x✝
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>-P y * P x ^ 3 * P z ^ 3 + 2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 * P z + 3 * P x * P y * P x ^ 2 * P z * P z ^ 2 + P x ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 3 - 2 * P y ^ 2 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 3 + W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) ^ 2 * P z ^ 4 + W'.a₁ * P y * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 3 * P z - W'.a₁ * P x * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z ^ 3 - W'.a₁ * P y ^ 2 * P x * P z ^ 4 - 2 * W'.a₂ * P x * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z + 2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 + W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) ^ 2 * P z ^ 6 - W'.a₃ * P y ^ 2 * P z ^ 6 - W'.a₄ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 6 * P z - W'.a₄ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z ^ 3 + W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 + W'.a₄ * P x * P y * P z * P z ^ 6 - 2 * W'.a₆ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 6 * P z ^ 3 + 2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 = (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 3
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => x - a) '' [[b, c]] = [[b - a, c - a]]
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<GOAL>∀ᵐ (ω : Ω) ∂μ, stoppedValue f (leastGE f r i) ω ≤ r + ↑R
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>hr : 0 ≤ r<VAR>hf0 : f 0 = 0<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>i : ℕ<VAR>ω : Ω<VAR>hbddω : ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>stoppedValue f (leastGE f r i) ω ≤ r + ↑R
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>g : γ → δ<VAR>f' : β' → α → δ<VAR>g' : β → β'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a<GOAL>image2 f' (g' '' t) ((fun a => a) '' s) = image2 f' (g' '' t) s
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : C < 0<VAR>hf : Tendsto f l (𝓝 C)<VAR>hg : Tendsto g l atBot<GOAL>Tendsto (fun x => f x * g x) l atTop
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>y ∈ closedBall x ε ↔ edist x y ≤ ε
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>δ / 4 + dist (x - const ι (3 / 4 * δ)) x ≤ δ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<GOAL>closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : dist x y < δ / 4<GOAL>closedBall (x - const ι (3 / 4 * δ)) (δ / 4) ⊆ interior s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : dist x y < δ / 4<VAR>z : ι → ℝ<VAR>hz : z ∈ closedBall (x - const ι (3 / 4 * δ)) (δ / 4)<VAR>i : ι<GOAL>z i < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : dist x y < δ / 4<VAR>z : ι → ℝ<VAR>hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4<VAR>i : ι<GOAL>z i < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>hxy : ‖x - y‖ < δ / 4<VAR>z : ι → ℝ<VAR>hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4<VAR>i : ι<GOAL>z i < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>hz : ‖x - const ι (3 / 4 * δ) - z‖ ≤ δ / 4<VAR>i : ι<VAR>hxy : ‖(x - y) i‖ ≤ δ / 4<GOAL>z i < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>i : ι<VAR>hxy : ‖(x - y) i‖ ≤ δ / 4<VAR>hz : ‖(x - const ι (3 / 4 * δ) - z) i‖ ≤ δ / 4<GOAL>z i < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>i : ι<VAR>hxy : |x i - y i| ≤ δ / 4<VAR>hz : |x i - 3 / 4 * δ - z i| ≤ δ / 4<GOAL>z i < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y✝ : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsLowerSet s<VAR>hx : x ∈ closure s<VAR>hδ : 0 < δ<VAR>y : ι → ℝ<VAR>hy : y ∈ s<VAR>z : ι → ℝ<VAR>i : ι<VAR>hxy : x i - y i ≤ δ / 4 ∧ y i - x i ≤ δ / 4<VAR>hz : x i - 3 / 4 * δ - z i ≤ δ / 4 ∧ z i - (x i - 3 / 4 * δ) ≤ δ / 4<GOAL>z i < y i
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>i : ι<GOAL>i ∈ ρ.finsupport x₀ ↔ i ∈ support fun i => (ρ i) x₀
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>x ∈ r • Icc a b ↔ x ∈ Icc (r • a) (r • b)
<VAR>α : Type u_1<VAR>K : Type u_2<VAR>inst✝ : LinearOrderedField K<VAR>a b r : K<VAR>hr : 0 < r<VAR>x : K<GOAL>(∃ y, (a ≤ y ∧ y ≤ b) ∧ r * y = x) ↔ r * a ≤ x ∧ x ≤ r * b
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K V : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K V < Module.rank K (V →ₗ[K] K)
<VAR>K✝ R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝³ : DivisionRing K✝<VAR>K V : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank K V = lift.{u, u} (Module.rank K V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f : α → β<VAR>a : α<VAR>s : Set α<VAR>x✝ : β<GOAL>x✝ ∈ f '' insert a s ↔ x✝ ∈ insert (f a) (f '' s)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>S : Set (Set V)<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected<VAR>s : Set V<VAR>sS : s ∈ S<GOAL>(induce (⋃₀ S) G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>S : Set (Set V)<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected<VAR>s : Set V<VAR>sS : s ∈ S<VAR>v : V<VAR>vs : v ∈ s<GOAL>(induce (⋃₀ S) G).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>S : Set (Set V)<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected<VAR>s : Set V<VAR>sS : s ∈ S<VAR>v : V<VAR>vs : v ∈ s<GOAL>∀ {v_1 : V}, v_1 ∈ ⋃₀ S → ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : v_1 ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨v_1, hv'⟩
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>S : Set (Set V)<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected<VAR>s : Set V<VAR>sS : s ∈ S<VAR>v : V<VAR>vs : v ∈ s<VAR>w : V<VAR>hw : w ∈ ⋃₀ S<GOAL>∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>S : Set (Set V)<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected<VAR>s : Set V<VAR>sS : s ∈ S<VAR>v : V<VAR>vs : v ∈ s<VAR>w : V<VAR>hw : ∃ t ∈ S, w ∈ t<GOAL>∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>S : Set (Set V)<VAR>Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty<VAR>Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected<VAR>s : Set V<VAR>sS : s ∈ S<VAR>v : V<VAR>vs : v ∈ s<VAR>w : V<VAR>t : Set V<VAR>tS : t ∈ S<VAR>wt : w ∈ t<GOAL>∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c✝ u a : αˣ<VAR>b c : α<VAR>h : ↑a * b = ↑a * c<GOAL>b = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : NegZeroClass G<VAR>inst✝ : NegZeroClass H<VAR>f : G → H<VAR>hf : f 0 = 0<VAR>hf' : ∀ (x : G), f (-x) = -f x<VAR>v : α →₀ G<VAR>x✝ : α<GOAL>(mapRange f hf (-v)) x✝ = (-mapRange f hf v) x✝
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>i : ℕ<GOAL>P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) = P.d (i + 1) i ≫ f i (i + 1)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<VAR>i : ℕ<VAR>this : (ComplexShape.down ℕ).next (i + 1) = i<GOAL>P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1)) ≫ f ((ComplexShape.down ℕ).next (i + 1)) (i + 1) = P.d (i + 1) i ≫ f i (i + 1)
<VAR>R : Type u_1<VAR>c₁ c₂ : R<GOAL>#ℍ[R,c₁,c₂] = #R ^ 4
<VAR>R : Type u_1<VAR>c₁ c₂ : R<GOAL>#(R × R × R × R) = #R ^ 4
<VAR>R : Type u_1<VAR>c₁ c₂ : R<GOAL>#R * (#R * (#R * #R)) = #R ^ 4
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<GOAL>IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Iio b = Ioi (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Iio b = Ioi (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Iio b = Ioi (a - b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t : Set α<VAR>f g : α → M<VAR>a✝ : α<VAR>U : Set α<VAR>s : Set M<VAR>a : M<GOAL>(U.mulIndicator fun x => a) ⁻¹' s ∈ {univ, U, Uᶜ, ∅}
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.6279, u_1} C<VAR>inst✝¹ : Category.{?u.6283, u_2} D<VAR>inst✝ : Category.{?u.6287, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E✝ : L.LeftExtension F<VAR>Y : D<VAR>E E' : L.LeftExtension F<VAR>φ : E ⟶ E'<VAR>G : CostructuredArrow L Y<GOAL>(E.hom.app G.left ≫ E.right.map G.hom) ≫ φ.right.app Y = E'.hom.app G.left ≫ E'.right.map G.hom
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.6279, u_1} C<VAR>inst✝¹ : Category.{?u.6283, u_2} D<VAR>inst✝ : Category.{?u.6287, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E✝ : L.LeftExtension F<VAR>Y : D<VAR>E E' : L.LeftExtension F<VAR>φ : E ⟶ E'<VAR>G : CostructuredArrow L Y<GOAL>(E.hom.app G.left ≫ E.right.map G.hom) ≫ φ.right.app Y = (E.hom ≫ ((whiskeringLeft C D H).obj L).map φ.right).app G.left ≫ E'.right.map G.hom
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<VAR>A : (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i => (μ (Ioc (u i) (v i))).toReal<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<VAR>A : (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i => (μ (Ioc (u i) (v i))).toReal<VAR>B : (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i => (μ (Ioc (v i) (u i))).toReal<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<VAR>A : (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i => (μ (Ioc (u i) (v i))).toReal<VAR>B : (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i => (μ (Ioc (v i) (u i))).toReal<GOAL>(fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ - ((μ (Ioc (u t) (v t))).toReal • c - (μ (Ioc (v t) (u t))).toReal • c)) =o[lt] fun t => (μ (Ioc (u t) (v t))).toReal • 1 - (μ (Ioc (v t) (u t))).toReal • 1
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<VAR>A : (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i => (μ (Ioc (u i) (v i))).toReal<VAR>B : (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i => (μ (Ioc (v i) (u i))).toReal<VAR>t : ι<GOAL>‖(μ (Ioc (u t) (v t))).toReal‖ ≤ ‖(μ (Ioc (u t) (v t))).toReal • 1 - (μ (Ioc (v t) (u t))).toReal • 1‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<VAR>A : (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i => (μ (Ioc (u i) (v i))).toReal<VAR>B : (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i => (μ (Ioc (v i) (u i))).toReal<VAR>t : ι<GOAL>‖(μ (Ioc (v t) (u t))).toReal‖ ≤ ‖(μ (Ioc (u t) (v t))).toReal • 1 - (μ (Ioc (v t) (u t))).toReal • 1‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝¹ : l'.IsMeasurablyGenerated<VAR>inst✝ : TendstoIxxClass Ioc l l'<VAR>hfm : StronglyMeasurableAtFilter f l' μ<VAR>hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)<VAR>hl : μ.FiniteAtFilter l'<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<VAR>hE : CompleteSpace E<VAR>A : (fun i => ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - (μ (Ioc (u i) (v i))).toReal • c) =o[lt] fun i => (μ (Ioc (u i) (v i))).toReal<VAR>B : (fun i => ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - (μ (Ioc (v i) (u i))).toReal • c) =o[lt] fun i => (μ (Ioc (v i) (u i))).toReal<VAR>t : ι<GOAL>∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - (μ (Ioc (u t) (v t))).toReal • c - (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - (μ (Ioc (v t) (u t))).toReal • c) = ∫ (x : ℝ) in u t..v t, f x ∂μ - ((μ (Ioc (u t) (v t))).toReal • c - (μ (Ioc (v t) (u t))).toReal • c)