ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : OpensMeasurableSpace X<VAR>hf : LocallyIntegrable f (μ.restrict s)<VAR>x : X<VAR>a✝ : x ∈ s<VAR>t : Set X<VAR>ht_mem : t ∈ 𝓝 x<VAR>ht_int : IntegrableOn f t (μ.restrict s)<VAR>u : Set X<VAR>hu_sub : u ⊆ t<VAR>hu_o : IsOpen u<VAR>hu_mem : x ∈ u<GOAL>IntegrableAtFilter f (𝓝[s] x) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : OpensMeasurableSpace X<VAR>hf : LocallyIntegrable f (μ.restrict s)<VAR>x : X<VAR>a✝ : x ∈ s<VAR>t : Set X<VAR>ht_mem : t ∈ 𝓝 x<VAR>ht_int : IntegrableOn f t (μ.restrict s)<VAR>u : Set X<VAR>hu_sub : u ⊆ t<VAR>hu_o : IsOpen u<VAR>hu_mem : x ∈ u<GOAL>IntegrableOn f (s ∩ u) μ
<VAR>n m : ℕ<VAR>i j : Fin n<GOAL>i.rev < j ↔ j.rev < i
<GOAL>(fun a => sup fun n => (HMul.hMul 0)^[n] a) = id
<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<VAR>a✝ : (HMul.hMul 0)^[n] a ≤ id a<GOAL>(HMul.hMul 0)^[n + 1] a ≤ id a
<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<VAR>a✝ : (HMul.hMul 0)^[n] a ≤ id a<GOAL>(HMul.hMul 0 ∘ (HMul.hMul 0)^[n]) a ≤ id a
<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<VAR>a✝ : (HMul.hMul 0)^[n] a ≤ id a<GOAL>0 * (HMul.hMul 0)^[n] a ≤ a
<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<VAR>a✝ : (HMul.hMul 0)^[n] a ≤ id a<GOAL>0 ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>image2 f s (⋂ i, t i) ⊆ ⋂ i, image2 f s (t i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s✝ : Set α<VAR>t✝ : Set β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>∀ x ∈ s, ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>(z - x) * f y < (z - y) * f x + (y - x) * f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>f y < ((z - y) * f x + (y - x) * f z) / (z - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 < (z - y) / (z - x)<VAR>hb : 0 < (y - x) / (z - x)<GOAL>f y < ((z - y) * f x + (y - x) * f z) / (z - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 < (z - y) / (z - x)<VAR>hb : 0 < (y - x) / (z - x)<GOAL>f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 < (z - y) / (z - x)<VAR>hb : 0 < (y - x) / (z - x)<GOAL>(z - y) / (z - x) + (y - x) / (z - x) = 1
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 < (z - y) / (z - x)<VAR>hb : 0 < (y - x) / (z - x)<GOAL>(z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>c : Ordinal.{max u v}<VAR>ho : Cardinal.lift.{v, u} o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c<VAR>h : o.blsub f = c<GOAL>c.cof ≤ Cardinal.lift.{v, u} o.card
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>max (max a b) c = max a (max b c)
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>a ≤ max (max a b) c
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>max b c ≤ max (max a b) c
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<GOAL>∀ {d : α}, a ≤ d → max b c ≤ d → max (max a b) c ≤ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>g : α →ₛ γ<VAR>b : β<VAR>c : γ<GOAL>↑(f.pair g) ⁻¹' {(b, c)} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>g : α →ₛ γ<VAR>b : β<VAR>c : γ<GOAL>↑(f.pair g) ⁻¹' {b} ×ˢ {c} = ↑f ⁻¹' {b} ∩ ↑g ⁻¹' {c}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsPreconnected (sphere x r)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>IsPreconnected (sphere x r)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r < 0<GOAL>IsPreconnected (sphere x r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t s : Set E<GOAL>ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t s : Set E<GOAL>(∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t) ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a b : ℝ<GOAL>volume (Ioc a b) = ofReal (b - a)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>f : α → β<VAR>k : ℕ<VAR>a : α<GOAL>map f (replicate k a) = replicate k (f a)
<VAR>m n✝ n a : ℕ<VAR>inst✝ : NeZero n<GOAL>(↑a).valMinAbs = ↑a ↔ a ≤ n / 2
<VAR>m n✝ n a : ℕ<VAR>inst✝ : NeZero n<VAR>ha : (↑a).valMinAbs = ↑a<GOAL>a ≤ n / 2
<VAR>m n✝ n a : ℕ<VAR>inst✝ : NeZero n<VAR>ha : (↑a).valMinAbs = ↑a<GOAL>(↑a).valMinAbs.natAbs ≤ n / 2
<VAR>m n k : ℕ<GOAL>(k * n + m).gcd n = m.gcd n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G✝ : Type u_10<VAR>H : Type u_11<VAR>G : Type u_12<VAR>inst✝ : Group G<VAR>x : Gˣ<GOAL>toUnits ↑x = x
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝ : LinearOrder γ<VAR>f : α → γ<GOAL>UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝¹ : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝ : LinearOrder γ<VAR>f : α → γ<GOAL>(∀ (y : γ), IsOpen (f ⁻¹' Iio y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Ici y)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>R : Type u_6<VAR>inst✝¹ : NonAssocRing R<VAR>inst✝ : Fintype R<VAR>p n : ℕ<GOAL>↑n = 0 ↔ addOrderOf 1 ∣ n
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>hscv : Convex ℝ s<VAR>this : Nonempty ↑s<VAR>p : V<VAR>hp : p ∈ s<GOAL>(intrinsicInterior ℝ s).Nonempty
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>hscv : Convex ℝ s<VAR>this : Nonempty ↑s<VAR>p : V<VAR>hp : p ∈ s<VAR>p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩<GOAL>(intrinsicInterior ℝ s).Nonempty
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : NormedSpace ℝ V<VAR>inst✝ : FiniteDimensional ℝ V<VAR>s : Set V<VAR>hscv : Convex ℝ s<VAR>this : Nonempty ↑s<VAR>p : V<VAR>hp : p ∈ s<VAR>p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩<GOAL>Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' (Subtype.val ⁻¹' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b a : α<VAR>s : Multiset α<GOAL>fold op b (a ::ₘ s) = op (fold op b s) a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>I : Set (ι × α)<GOAL>(Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>I : Set (ι × α)<GOAL>(∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I))) ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : ι → Matroid α<VAR>I : Set (ι × α)<VAR>a✝ : ι<GOAL>Prod.mk a✝ ⁻¹' I = Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)
<VAR>M✝ : Type u_1<VAR>N✝ : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>M : Type u_11<VAR>N : Type u_12<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : SMul M N<VAR>inst✝ : SMulCommClass M N N<VAR>x : M<VAR>y : N<GOAL>y * x • 1 = x • y
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>σ : Type u<VAR>x✝ : Nonempty (Cardinal.{u} ↪ σ)<VAR>f : Cardinal.{u} → σ<VAR>hf : Injective f<VAR>g : σ → Cardinal.{u} := invFun f<VAR>x : σ<VAR>hx : g x = 2 ^ sum g<VAR>this : g x ≤ sum g<GOAL>2 ^ sum g > sum g
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : HasKernel f✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : Mono g<GOAL>kernel.ι (f ≫ g) ≫ f = 0
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>X✝ Y✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝² : HasKernel f✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : Mono g<GOAL>(kernel.ι (f ≫ g) ≫ f) ≫ g = 0 ≫ g
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n m : ℕ<VAR>hn : 0 < n<GOAL>m.gcd n * addOrderOf ↑(↑m / ↑n * p) = n
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n m : ℕ<VAR>hn : 0 < n<GOAL>m.gcd n * (addOrderOf ↑(p / ↑n) / (addOrderOf ↑(p / ↑n)).gcd m) = n
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : 𝕜<VAR>hp : Fact (0 < p)<VAR>n m : ℕ<VAR>hn : 0 < n<GOAL>IsOfFinAddOrder ↑(p / ↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>f =ᶠ[ae (μ.restrict s)] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x<GOAL>∀ᵐ (x : α) ∂μ.restrict s, f x = g x
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<GOAL>IsPathConnected sᶜ
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<GOAL>IsPathConnected sᶜ
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<GOAL>IsPathConnected sᶜ
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha hb : a ∈ sᶜ<GOAL>JoinedIn sᶜ a a
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>B : {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>B : {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>t : ℝ<VAR>ht : t ∈ ({t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty} ∪ {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty})ᶜ<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>B : {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>t : ℝ<VAR>ht : t ∈ ({t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty} ∪ {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty})ᶜ<VAR>z : E := c + t • y<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>B : {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>t : ℝ<VAR>z : E := c + t • y<VAR>ht : [c + x-[ℝ]c + t • y] ∩ s = ∅ ∧ [c - x-[ℝ]c + t • y] ∩ s = ∅<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>B : {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>t : ℝ<VAR>z : E := c + t • y<VAR>ht : [c + x-[ℝ]c + t • y] ∩ s = ∅ ∧ [c - x-[ℝ]c + t • y] ∩ s = ∅<VAR>JA : JoinedIn sᶜ a z<GOAL>JoinedIn sᶜ a b
<VAR>E : Type u_1<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<VAR>this : Nontrivial E<VAR>a : E<VAR>ha : a ∈ sᶜ<VAR>b : E<VAR>hb : b ∈ sᶜ<VAR>hab : a ≠ b<VAR>c : E := 2⁻¹ • (a + b)<VAR>x : E := 2⁻¹ • (b - a)<VAR>Ia : c - x = a<VAR>Ib : c + x = b<VAR>x_ne_zero : x ≠ 0<VAR>y : E<VAR>hy : LinearIndependent ℝ ![x, y]<VAR>A : {t | ([c + x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>B : {t | ([c - x-[ℝ]c + t • y] ∩ s).Nonempty}.Countable<VAR>t : ℝ<VAR>z : E := c + t • y<VAR>ht : [c + x-[ℝ]c + t • y] ∩ s = ∅ ∧ [c - x-[ℝ]c + t • y] ∩ s = ∅<VAR>JA : JoinedIn sᶜ a z<VAR>JB : JoinedIn sᶜ b z<GOAL>JoinedIn sᶜ a b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>hf : AEStronglyMeasurable f μ<VAR>hg : AEStronglyMeasurable g μ<VAR>hp : 1 ≤ p<GOAL>eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'✝<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'✝<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Nontrivial R<VAR>M' : Submodule R M<GOAL>Module.rank R (M ⧸ M') + Module.rank R ↥M' ≤ Module.rank R M
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'✝<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'✝<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Nontrivial R<VAR>M' : Submodule R M<GOAL>(⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'✝<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'✝<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Nontrivial R<VAR>M' : Submodule R M<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>(⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'✝<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'✝<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Nontrivial R<VAR>M' : Submodule R M<VAR>this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>(⨆ ι, #↑↑ι) + ⨆ ι, #↑↑ι ≤ Module.rank R M
<VAR>R S : Type u<VAR>M : Type v<VAR>M'✝ : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'✝<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'✝<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Nontrivial R<VAR>M' : Submodule R M<VAR>this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>⨆ i, ⨆ j, #↑↑i + #↑↑j ≤ Module.rank R M