ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>a b c d : α<GOAL>b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>a ≠ b → a ∈ s → a ∈ s.erase b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>htμ : t ⟂ᵥ μ.toENNRealVectorMeasure<GOAL>(t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>f : α → ℝ<VAR>hf : Measurable f<VAR>htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ<GOAL>(t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x)) ⟂ₘ t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x)
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>p : Homotopic.Quotient as bs<GOAL>(pi fun i => proj i p) = p
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>a✝ : Path as bs<GOAL>(pi fun i => proj i ⟦a✝⟧) = ⟦a✝⟧
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>a✝ : Path as bs<GOAL>(pi fun i => ⟦a✝.map ⋯⟧) = ⟦a✝⟧
<VAR>ι : Type u_1<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>as bs cs : (i : ι) → X i<VAR>a✝ : Path as bs<GOAL>⟦Path.pi fun i => a✝.map ⋯⟧ = ⟦a✝⟧
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>((HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 0 1 2 isoOneCocycles.proof_2 isoOneCocycles.proof_3).hom ≫ cyclesMap { τ₁ := ↑(zeroCochainsLequiv A), τ₂ := ↑(oneCochainsLequiv A), τ₃ := ↑(twoCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫ (shortComplexH1 A).moduleCatCyclesIso.hom) ≫ ModuleCat.ofHom (oneCocycles A).subtype = iCocycles A 1 ≫ ↑(oneCochainsLequiv A)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>(HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 0 1 2 isoOneCocycles.proof_2 isoOneCocycles.proof_3).hom ≫ cyclesMap { τ₁ := ↑(zeroCochainsLequiv A), τ₂ := ↑(oneCochainsLequiv A), τ₃ := ↑(twoCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫ (shortComplexH1 A).moduleCatCyclesIso.hom ≫ ModuleCat.ofHom (oneCocycles A).subtype = iCocycles A 1 ≫ ↑(oneCochainsLequiv A)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>(HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 0 1 2 isoOneCocycles.proof_2 isoOneCocycles.proof_3).hom ≫ cyclesMap { τ₁ := ↑(zeroCochainsLequiv A), τ₂ := ↑(oneCochainsLequiv A), τ₃ := ↑(twoCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫ (shortComplexH1 A).iCycles = iCocycles A 1 ≫ ↑(oneCochainsLequiv A)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>x y : k<GOAL>{ toFun := (↑__src✝).toFun, map_one' := ⋯ }.toFun (x * y) = { toFun := (↑__src✝).toFun, map_one' := ⋯ }.toFun x * { toFun := (↑__src✝).toFun, map_one' := ⋯ }.toFun y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>μ K ≤ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : μ.InnerRegularCompactLTTop<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>K : Set α<VAR>hK : IsCompact K<GOAL>⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), μ U ≤ μ K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AlgHomClass F R A B<VAR>φ ψ : F<VAR>S T : Subalgebra R A<VAR>hS : Set.EqOn ⇑φ ⇑ψ ↑S<VAR>hT : Set.EqOn ⇑φ ⇑ψ ↑T<GOAL>Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AlgHomClass F R A B<VAR>φ ψ : F<VAR>S T : Subalgebra R A<VAR>hS : S ≤ equalizer φ ψ<VAR>hT : T ≤ equalizer φ ψ<GOAL>S ⊔ T ≤ equalizer φ ψ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<GOAL>DifferentiableOn 𝕜 f univ ↔ Differentiable 𝕜 f
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ<VAR>f : r ⟶ s<GOAL>((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).val).map f ≫ (fun r => X.toΓSpecCApp (unop r)) s = (fun r => X.toΓSpecCApp (unop r)) r ≫ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).map f
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ<VAR>f : r ⟶ s<GOAL>toOpen (↑(Γ.obj (op X))) (basicOpen (unop r)) ≫ ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).val).map f ≫ (fun r => X.toΓSpecCApp (unop r)) s = toOpen (↑(Γ.obj (op X))) (basicOpen (unop r)) ≫ (fun r => X.toΓSpecCApp (unop r)) r ≫ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).map f
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ<VAR>f : r ⟶ s<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen (unop r)) ≫ ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).val).map f) ≫ X.toΓSpecCApp (unop s) = (toOpen (↑(Γ.obj (op X))) (basicOpen (unop r)) ≫ X.toΓSpecCApp (unop r)) ≫ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).map f
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ<VAR>f : r ⟶ s<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen (unop r)) ≫ ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).val).map f) ≫ X.toΓSpecCApp (unop s) = X.toToΓSpecMapBasicOpen (unop r) ≫ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).map f
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ<VAR>f : r ⟶ s<VAR>e_1✝ : (CommRingCat.of ↑(Γ.obj (op X)) ⟶ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).obj s) = (CommRingCat.of ↑(Γ.obj (op X)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))<GOAL>X.toToΓSpecMapBasicOpen (unop r) ≫ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).map f = X.toToΓSpecMapBasicOpen (unop s)
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ<VAR>f : r ⟶ s<VAR>e_1✝ : (CommRingCat.of ↑(Γ.obj (op X)) ⟶ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).obj s) = (CommRingCat.of ↑(Γ.obj (op X)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen (unop s))))<GOAL>X.toToΓSpecMapBasicOpen (unop s) = X.toToΓSpecMapBasicOpen (unop r) ≫ ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).val).map f
<VAR>G : Type u''<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type w<VAR>inst✝¹ : Ring R<VAR>inst✝ : AddCommGroup M<VAR>module_M : Module R M<VAR>p p' : Submodule R M<VAR>r : R<VAR>x y : M<VAR>hy : y ∈ p<GOAL>x - y ∈ p ↔ x ∈ p
<VAR>R S T : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hf : f.FinitePresentation<VAR>hg : g.FinitePresentation<GOAL>(g.comp f).FinitePresentation
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ <+ l₂<GOAL>countP p l₁ ≤ countP p l₂
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l₁ l₂ : List α<VAR>s : l₁ <+ l₂<GOAL>(List.filter p l₁).length ≤ (List.filter p l₂).length
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>P : Perm α → Prop<VAR>f : Perm α<GOAL>P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Finite α<VAR>P : Perm α → Prop<VAR>f : Perm α<VAR>val✝ : Fintype α<GOAL>P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NontriviallyNormedField α<GOAL>(𝓝[{x | IsUnit x}] 0).NeBot
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι✝ : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>β : α → Type u_10<VAR>ι : Sort u_11<VAR>inst✝ : (i : α) → SupSet (β i)<VAR>f : ι → (a : α) → β a<VAR>a : α<GOAL>(⨆ i, f i) a = ⨆ i, f i a
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι✝ : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>α : Type u_9<VAR>β : α → Type u_10<VAR>ι : Sort u_11<VAR>inst✝ : (i : α) → SupSet (β i)<VAR>f : ι → (a : α) → β a<VAR>a : α<GOAL>sSup (range ((fun f => f a) ∘ f)) = sSup (range fun i => f i a)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>a :: l₁ ~ l₂ ↔ a ∈ l₂ ∧ l₁ ~ l₂.erase a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : a :: l₁ ~ l₂<GOAL>a ∈ l₂ ∧ l₁ ~ l₂.erase a
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<VAR>h : a :: l₁ ~ l₂<VAR>this : a ∈ l₂<GOAL>a ∈ l₂ ∧ l₁ ~ l₂.erase a
<VAR>u v m n✝ n : ℤ<GOAL>¬2 ∣ 2 * n + 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<GOAL>0 ∪ s = s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>Disjoint (span R (range (u ∘ Sum.inr))) (span R (range (⇑S.f ∘ v)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ⇑S.f))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>Disjoint (span R (range (u ∘ Sum.inr))) (LinearMap.ker S.g)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p1 : P<VAR>hp1 : p1 ∈ s<VAR>p2 p : P<GOAL>p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p2 -ᵥ p1) +ᵥ p0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s<VAR>p2 p : P<GOAL>p ∈ affineSpan k (insert p2 ↑s) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p2 -ᵥ p1) +ᵥ p0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p1 : P<VAR>hp1 : p1 ∈ ↑s<VAR>p2 p : P<GOAL>(∃ y ∈ Submodule.span k {p2 -ᵥ p1}, ∃ z ∈ s.direction, y + z = p -ᵥ p1) ↔ ∃ r, ∃ p0 ∈ s, p = r • (p2 -ᵥ p1) +ᵥ p0
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>a : α<VAR>b : β<VAR>l : List (α × β)<GOAL>((a, b) :: l).unzip.1.zip ((a, b) :: l).unzip.2 = (a, b) :: l
<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>hs : StarConvex 𝕜 x s<VAR>z : E<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>y' : E<VAR>hy' : y' ∈ s<GOAL>(fun x => z + x) (a • x + b • y') = a • (z + x) + b • (fun x => z + x) y'
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.leadingCoeff = f.trailingCoeff
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>StructureSheaf.toStalk (↑(CommRingCat.of (A⁰_ f))) ((toSpec 𝒜 f).val.base x) ≫ LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>StructureSheaf.toOpen ↑(CommRingCat.of (A⁰_ f)) ⊤ ≫ (Spec.structureSheaf ↑(CommRingCat.of (A⁰_ f))).presheaf.germ ⟨(toSpec 𝒜 f).val.base x, True.intro⟩ ≫ LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>StructureSheaf.toOpen (A⁰_ f) ⊤ ≫ (Spec.structureSheaf (A⁰_ f)).presheaf.germ ⟨(toSpec 𝒜 f).val.base x, True.intro⟩ ≫ LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>StructureSheaf.toOpen (A⁰_ f) ⊤ ≫ (toSpec 𝒜 f).val.c.app (op ⊤) ≫ (Proj.restrict ⋯).presheaf.germ ⟨x, True.intro⟩ = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑(Proj.restrict ⋯).toTopCat<GOAL>awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.germ ((fun x => ⟨↑x, ⋯⟩) ⟨x, True.intro⟩) = awayToΓ 𝒜 f ≫ (Proj.restrict ⋯).presheaf.Γgerm x
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>b < a * b ↔ 1 < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : LinearOrderedField β<VAR>inst✝ : OrderTopology β<VAR>hk : Tendsto k l atTop<VAR>hf : SuperpolynomialDecay l k f<GOAL>SuperpolynomialDecay l k (k⁻¹ * f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂
<VAR>x : ℝ<GOAL>sin (x + π / 2) = cos x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι✝ : Sort u_5<VAR>ι'✝ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ' : ι'✝ → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f g✝ s✝ t : ι✝ → α<VAR>a b : α<VAR>ι : Type u_9<VAR>ι' : Type u_10<VAR>g : ι' → α<VAR>e : ι ≃ ι'<VAR>s : Set ι'<GOAL>⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderBot α<VAR>a : α<GOAL>Ico ⊥ a = Iio a
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>l : List α<VAR>k : Nat<GOAL>x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l.get? i = some x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<GOAL>Periodic f (2 • c)
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>inst✝ : Algebra.IsAlgebraic K ↥E1<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E1 E2 : IntermediateField K L<VAR>inst✝ : Algebra.IsAlgebraic K ↥E1<VAR>this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra<GOAL>(E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>p : α → Prop<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>(∀ᵐ (x : α) ∂c • μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>hst : s =ᶠ[ae μ] t<GOAL>∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>hr : IsUnit r<GOAL>p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>hr : IsUnit r<GOAL>(p.scaleRoots r).scaleRoots ↑hr.unit⁻¹ ∣ (q.scaleRoots r).scaleRoots ↑hr.unit⁻¹ → p ∣ q
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>inst✝¹ : UniformSpace F<VAR>inst✝ : UniformAddGroup F<VAR>𝔖 : Set (Set E)<GOAL>instUniformSpace σ F 𝔖 = UniformSpace.comap DFunLike.coe (UniformOnFun.uniformSpace E F 𝔖)
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>f.closure.IsClosed
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>_root_.IsClosed ↑f.graph.topologicalClosure
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<VAR>x y : G<GOAL>(fun x => (f x) m) (x + y) = (fun x => (f x) m) x + (fun x => (f x) m) y
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<VAR>c : 𝕜<VAR>x : G<GOAL>{ toFun := fun x => (f x) m, map_add' := ⋯ }.toFun (c • x) = (RingHom.id 𝕜) c • { toFun := fun x => (f x) m, map_add' := ⋯ }.toFun x
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<VAR>x : G<GOAL>‖{ toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖