ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hyz : ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (z -ᵥ p₂_1)<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)<GOAL>s.WSameSide x z
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)<GOAL>y -ᵥ p₂ = 0 → x -ᵥ p₁ = 0 ∨ z -ᵥ p₃ = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)<VAR>h : y -ᵥ p₂ = 0<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y z : P<VAR>hy : y ∉ s<VAR>p₁ : P<VAR>hp₁ : p₁ ∈ s<VAR>p₂ : P<VAR>hp₂ : p₂ ∈ s<VAR>hxy : SameRay R (x -ᵥ p₁) (y -ᵥ p₂)<VAR>p₃ : P<VAR>hp₃ : p₃ ∈ s<VAR>hyz : SameRay R (y -ᵥ p₂) (z -ᵥ p₃)<VAR>h : y = p₂<GOAL>False
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsOpen (⇑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier)
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsOpen (⇑(TopCat.homeoOfIso (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) f.val g.val)) ∘ ⇑(colimit.ι (parallelPair ((SheafedSpace.forget CommRingCat).map f.val) ((SheafedSpace.forget CommRingCat).map g.val)) WalkingParallelPair.one) ⁻¹' (⇑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsOpen (⇑(colimit.ι (parallelPair ((SheafedSpace.forget CommRingCat).map f.val) ((SheafedSpace.forget CommRingCat).map g.val)) WalkingParallelPair.one ≫ (PreservesCoequalizer.iso (SheafedSpace.forget CommRingCat) f.val g.val).hom) ⁻¹' (⇑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsOpen (⇑((SheafedSpace.forget CommRingCat).map (coequalizer.π f.val g.val)) ⁻¹' (⇑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsOpen (⇑(coequalizer.π f.val g.val).base ⁻¹' (⇑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier))
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsOpen (imageBasicOpen f g U s).carrier
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsIso (f ≫ g)<GOAL>IsIso g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>h : Y✝ ⟶ Z✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsIso (f ≫ g)<GOAL>IsIso (inv f ≫ f ≫ g)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>W.Ψ₂Sq.leadingCoeff = 4
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>f : M ↪[L] N<VAR>htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))<GOAL>∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>f : M ↪[L] N<VAR>htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N), φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))<GOAL>∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<GOAL>WithSeminorms (gaugeSeminormFamily 𝕜 E)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ (gaugeSeminormFamily 𝕜 E).basisSets) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s<GOAL>∃ i' ∈ (gaugeSeminormFamily 𝕜 E).basisSets, id i' ⊆ id s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets<GOAL>∃ i, (0 ∈ i ∧ IsOpen i ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>hs : s ∈ (gaugeSeminormFamily 𝕜 E).basisSets<GOAL>0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>hs : ∃ i r, 0 < r ∧ s = (i.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r<GOAL>0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>t : Finset (AbsConvexOpenSets 𝕜 E)<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>0 ∈ (t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r ∧ IsOpen ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧ Balanced 𝕜 ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r) ∧ Convex ℝ ((t.sup (gaugeSeminormFamily 𝕜 E)).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>t : Finset (AbsConvexOpenSets 𝕜 E)<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>0 ∈ ⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r ∧ IsOpen (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧ Balanced 𝕜 (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r) ∧ Convex ℝ (⋂ i ∈ t, (gaugeSeminormFamily 𝕜 E i).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>t : Finset (AbsConvexOpenSets 𝕜 E)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>S : AbsConvexOpenSets 𝕜 E<VAR>x✝ : S ∈ t<GOAL>IsOpen ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>t : Finset (AbsConvexOpenSets 𝕜 E)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>S : AbsConvexOpenSets 𝕜 E<VAR>x✝ : S ∈ t<VAR>hr' : r = ‖↑r‖ * 1<GOAL>IsOpen ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>t : Finset (AbsConvexOpenSets 𝕜 E)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>S : AbsConvexOpenSets 𝕜 E<VAR>x✝ : S ∈ t<VAR>hr' : r = ‖↑r‖ * 1<VAR>hr'' : ↑r ≠ 0<GOAL>IsOpen ((gaugeSeminormFamily 𝕜 E S).ball 0 r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>inst✝¹⁰ : RCLike 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module ℝ E<VAR>inst✝⁵ : IsScalarTower ℝ 𝕜 E<VAR>inst✝⁴ : ContinuousSMul ℝ E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>inst✝¹ : SMulCommClass ℝ 𝕜 E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>t : Finset (AbsConvexOpenSets 𝕜 E)<VAR>r : ℝ<VAR>hr : 0 < r<VAR>S : AbsConvexOpenSets 𝕜 E<VAR>x✝ : S ∈ t<VAR>hr' : r = ‖↑r‖ * 1<VAR>hr'' : ↑r ≠ 0<GOAL>IsOpen (↑r • ↑S)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>i : IsLimit c<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>hg : Mono g<VAR>h : X ⟶ Z<VAR>hh : h = f ≫ g<VAR>s : KernelFork h<GOAL>Fork.ι s ≫ f = Fork.ι s ≫ 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : KernelFork f<VAR>i : IsLimit c<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>hg : Mono g<VAR>h : X ⟶ Z<VAR>hh : h = f ≫ g<VAR>s : KernelFork h<GOAL>Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<GOAL>M ∈ Set.range ⇑(scalar n) ↔ ∀ (t : TransvectionStruct n R), Commute t.toMatrix M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>h : M ∈ Set.range ⇑(scalar n)<VAR>t : TransvectionStruct n R<GOAL>Commute t.toMatrix M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M<VAR>t : TransvectionStruct n R<GOAL>Commute t.toMatrix M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M<VAR>t : TransvectionStruct n R<GOAL>Commute (stdBasisMatrix t.i t.j t.c) M
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>M : Matrix n n R<VAR>h : ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M<VAR>t : TransvectionStruct n R<GOAL>stdBasisMatrix t.i t.j t.c = t.c • stdBasisMatrix t.i t.j 1
<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>p : α → Prop<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>h : ∀ᵐ (x : α) ∂μ, p x<VAR>c : R<GOAL>(c • μ) {a | ¬p a} = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s✝ : Set E<VAR>s : Set F<VAR>f : E →ₗ[𝕜] F<VAR>hs : StarConvex 𝕜 (f x) s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ⇑f ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ z : E<VAR>s✝ : Set E<VAR>s : Set F<VAR>f : E →ₗ[𝕜] F<VAR>hs : StarConvex 𝕜 (f x) s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b✝ a b : α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ (s.erase a).erase b ↔ x ∈ (s.erase b).erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b✝ a b : α<VAR>s : Finset α<VAR>x : α<GOAL>(x ≠ b ∧ x ≠ a) ∧ x ∈ s ↔ (x ≠ a ∧ x ≠ b) ∧ x ∈ s
<VAR>q : ℚ<VAR>x y : ℝ<GOAL>x * y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast
<VAR>q : ℚ<VAR>x y : ℝ<GOAL>x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast
<VAR>q rx ry : ℚ<GOAL>↑rx * ↑ry ∈ Set.range Rat.cast
<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>x : X<GOAL>IsOpen {x} ↔ 𝓝[≠] x = ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Group α<VAR>n : ℤ<VAR>a : α<GOAL>IsSquare (a ^ (n + n))
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>x✝ : ∃ c, ↑c * x = ↑c * y<VAR>c : ↥S<VAR>h : f.toMap (↑c * x) = f.toMap (↑c * y)<GOAL>f.toMap x = f.toMap y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>x y : M<VAR>x✝ : ∃ c, ↑c * x = ↑c * y<VAR>c : ↥S<VAR>h : f.toMap ↑c * f.toMap x = f.toMap ↑c * f.toMap y<GOAL>f.toMap x = f.toMap y
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>h : HasProd (fun n => f (n + 1)) m<GOAL>HasProd f (f 0 * m)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : NormedAddCommGroup E''<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E''<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : TopologicalAddGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : TopologicalSpace P<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (range fun x => ‖g x‖)<VAR>hf : Integrable f μ<VAR>hg : Continuous g<GOAL>Continuous (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : NormedAddCommGroup E''<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E''<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : TopologicalAddGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : TopologicalSpace P<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (range fun x => ‖g x‖)<VAR>hf : Integrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<GOAL>ContinuousAt (f ⋆[L, μ] g) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : NormedAddCommGroup E''<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E''<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : TopologicalAddGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : TopologicalSpace P<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (range fun x => ‖g x‖)<VAR>hf : Integrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<VAR>this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖<GOAL>ContinuousAt (f ⋆[L, μ] g) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : NormedAddCommGroup E''<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E''<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : TopologicalAddGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : TopologicalSpace P<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (range fun x => ‖g x‖)<VAR>hf : Integrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<VAR>this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖<GOAL>∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun a => (L (f a)) (g (x - a))) μ
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : NormedAddCommGroup E''<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E''<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : TopologicalAddGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : TopologicalSpace P<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (range fun x => ‖g x‖)<VAR>hf : Integrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<VAR>this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖<GOAL>Integrable (fun a => ‖L‖ * ‖f a‖ * ⨆ i, ‖g i‖) μ