ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<VAR>hxy' : x' ≠ y'<GOAL>a • f x' + b • f y' < f (a • x' + b • y')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η : Kernel α β<VAR>μ ν : Measure α<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : SFinite ν<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<GOAL>(μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ✝ : Measure α<VAR>κ✝ η : Kernel α β<VAR>μ ν : Measure α<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : SFinite ν<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<GOAL>(Kernel.const Unit μ ⊗ₖ Kernel.prodMkLeft Unit κ + Kernel.const Unit ν ⊗ₖ Kernel.prodMkLeft Unit κ) () = μ ⊗ₘ κ + ν ⊗ₘ κ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ ψ : MvPolynomial σ R<GOAL>IsWeightedHomogeneous w ((weightedHomogeneousComponent w n) φ) n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s t : Multiset α<VAR>h : s ≤ t<GOAL>countP p s ≤ countP p t
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹¹ : Category.{u_3, u_1} C<VAR>inst✝¹⁰ : Category.{u_4, u_2} D<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>inst✝⁸ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁷ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁶ : F.PreservesZeroMorphisms<VAR>inst✝⁵ : S₁.HasHomology<VAR>inst✝⁴ : S₂.HasHomology<VAR>inst✝³ : (S₁.map F).HasHomology<VAR>inst✝² : (S₂.map F).HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S₁<VAR>inst✝ : F.PreservesLeftHomologyOf S₂<GOAL>F.map (homologyMap φ) ≫ (S₂.mapHomologyIso F).inv = (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>i : ℕ<VAR>x : X i<VAR>hx : ⟨i, x⟩.fst ≤ 0<VAR>j : ℕ<VAR>y : X j<VAR>hy : ⟨j, y⟩.fst ≤ 0<GOAL>inductiveLimitDist f ⟨i, x⟩ ⟨j, y⟩ = dist (leRecOn hx (fun {k} => f k) ⟨i, x⟩.snd) (leRecOn hy (fun {k} => f k) ⟨j, y⟩.snd)
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>j : ℕ<VAR>y : X j<VAR>hy : ⟨j, y⟩.fst ≤ 0<VAR>x : X 0<VAR>hx : ⟨0, x⟩.fst ≤ 0<GOAL>inductiveLimitDist f ⟨0, x⟩ ⟨j, y⟩ = dist (leRecOn hx (fun {k} => f k) ⟨0, x⟩.snd) (leRecOn hy (fun {k} => f k) ⟨j, y⟩.snd)
<VAR>X : ℕ → Type u<VAR>inst✝ : (n : ℕ) → MetricSpace (X n)<VAR>f : (n : ℕ) → X n → X (n + 1)<VAR>I : ∀ (n : ℕ), Isometry (f n)<VAR>x : X 0<VAR>hx : ⟨0, x⟩.fst ≤ 0<VAR>y : X 0<VAR>hy : ⟨0, y⟩.fst ≤ 0<GOAL>inductiveLimitDist f ⟨0, x⟩ ⟨0, y⟩ = dist (leRecOn hx (fun {k} => f k) ⟨0, x⟩.snd) (leRecOn hy (fun {k} => f k) ⟨0, y⟩.snd)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>c : Sigma β<VAR>l : List (Sigma β)<VAR>h : (c :: l).NodupKeys<GOAL>{ entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := ⋯ }
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>A✝ B✝ : C<VAR>f✝ g✝ : A✝ ⟶ B✝<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : HasReflexiveCoequalizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>r : B ⟶ A<VAR>rf : r ≫ f = 𝟙 B<VAR>rg : r ≫ g = 𝟙 B<GOAL>HasCoequalizer f g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>A✝ B✝ : C<VAR>f✝ g✝ : A✝ ⟶ B✝<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>inst✝ : HasReflexiveCoequalizers C<VAR>A B : C<VAR>f g : A ⟶ B<VAR>r : B ⟶ A<VAR>rf : r ≫ f = 𝟙 B<VAR>rg : r ≫ g = 𝟙 B<VAR>this : IsReflexivePair f g := IsReflexivePair.mk' r rf rg<GOAL>HasCoequalizer f g
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>‖∫ (x : X), f x ∂μ‖ ≤ (μ Set.univ).toReal * ‖f‖
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>∫ (x : X), ‖f x‖ ∂μ ≤ ∫ (x : X), ‖f‖ ∂μ
<VAR>X : Type u_1<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SecondCountableTopology E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ E<GOAL>Integrable (fun x => ‖f x‖) μ
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>(monomial (Finsupp.single n e + s)) a = X n ^ e * (monomial s) a
<GOAL>ClosedEmbedding ⇑natUnionInftyEmbedding
<GOAL>Function.Injective ⇑natUnionInftyEmbedding
<GOAL>IsClosedMap ⇑natUnionInftyEmbedding
<VAR>x : ℝ*<GOAL>x⁻¹⁻¹.Infinitesimal ∧ x⁻¹⁻¹ < 0 ↔ x.Infinitesimal ∧ x < 0
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : WithLp p (α × β)<GOAL>edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>hp : Fact (1 ≤ ⊤)<VAR>x y : WithLp ⊤ (α × β)<GOAL>edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y) ≤ ↑1 * edist x y
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : WithLp p (α × β)<VAR>h : 1 ≤ p.toReal<GOAL>edist ((WithLp.equiv p (α × β)) x) ((WithLp.equiv p (α × β)) y) ≤ ↑1 * edist x y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) = C 0 * Y ^ 3 + C 1 * Y ^ 2 + C (C 0 * X ^ 3 + C 0 * X ^ 2 + C W.a₁ * X + C W.a₃) * Y + C (C (-1) * X ^ 3 + C (-W.a₂) * X ^ 2 + C (-W.a₄) * X + C (-W.a₆))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)) = 0 * Y ^ 3 + 1 * Y ^ 2 + (0 * C X ^ 3 + 0 * C X ^ 2 + C (C W.a₁) * C X + C (C W.a₃)) * Y + (-1 * C X ^ 3 + -C (C W.a₂) * C X ^ 2 + -C (C W.a₄) * C X + -C (C W.a₆))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, b ≤ a → b = a<GOAL>s.erase a ⊓ Ici a = s
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<GOAL>(fun n => (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) =o[atTop] Nat.cast
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : Tendsto (fun i => ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))<GOAL>(fun n => (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) =o[atTop] Nat.cast
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : Tendsto (fun i => ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))<GOAL>(fun n => (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) = fun n => ∑ i ∈ range n, ((∫ (a : Ω), truncation (X i) (↑i) a) - ∫ (a : Ω), X 0 a)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : Tendsto (fun i => ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))<VAR>n : ℕ<GOAL>(∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a = ∑ i ∈ range n, ((∫ (a : Ω), truncation (X i) (↑i) a) - ∫ (a : Ω), X 0 a)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : Tendsto (fun i => ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))<VAR>n : ℕ<GOAL>∫ (a : Ω), ∑ c ∈ range n, truncation (X c) (↑c) a = ∑ x ∈ range n, ∫ (a : Ω), truncation (X x) (↑x) a
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsProbabilityMeasure ℙ<VAR>X : ℕ → Ω → ℝ<VAR>hint : Integrable (X 0) ℙ<VAR>hindep : Pairwise fun i j => IndepFun (X i) (X j) ℙ<VAR>hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ<VAR>hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω<VAR>A : Tendsto (fun i => ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))<VAR>n i : ℕ<VAR>x✝ : i ∈ range n<GOAL>Integrable (truncation (X i) ↑i) ℙ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>f g : ↥(simpleFunc G p μ)<GOAL>↑↑↑f ≤ᶠ[ae μ] ↑↑↑g ↔ f ≤ g
<VAR>n : ℤ<VAR>g : SL(2, ℤ)<VAR>j : Fin 2<GOAL>↑(T ^ n * g) 1 j = ↑g 1 j
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>s : Set Ω<VAR>i : ι<GOAL>MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>r : R<GOAL>(optionEquivRight R S₁) (C r) = C (Polynomial.C r)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>ha : a ∈ s<GOAL>a ^ 0 ∈ s ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>ha : a ∈ s<GOAL>1 ∈ s ^ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n✝ : ℕ<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>a ^ (n + 1) ∈ s ^ (n + 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n✝ : ℕ<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>a ^ n * a ∈ s ^ (n + 1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝ : Category.{u_3, u_2} A<VAR>G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj : G ⊣ sheafToPresheaf J A<VAR>P₁ P₂ : Cᵒᵖ ⥤ A<VAR>f : P₁ ⟶ P₂<GOAL>J.W f ↔ IsIso (G.map f)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝ : Category.{u_3, u_2} A<VAR>G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A<VAR>adj : G ⊣ sheafToPresheaf J A<VAR>P₁ P₂ : Cᵒᵖ ⥤ A<VAR>f : P₁ ⟶ P₂<GOAL>LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) f ↔ IsIso (G.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>s : Set β<VAR>t : Set γ<VAR>hf : Surjective f<VAR>hg : SurjOn g s t<GOAL>SurjOn (g ∘ f) (f ⁻¹' s) t
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>𝕜 : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : SMulCommClass ℂ 𝕜 E<VAR>c : 𝕜<GOAL>mellin (fun t => c • f t) s = c • mellin f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝² : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝² : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>(⨆ i, f i) ⊓ ⨆ i, g i ≤ ⨆ i, f i ⊓ g i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝² : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>⨆ i, f i.1 ⊓ g i.2 ≤ ⨆ i, f i ⊓ g i
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝² : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>i : ι × ι<GOAL>∃ i', f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝² : Frame α<VAR>s t : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f g : ι → α<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>i : ι × ι<VAR>j : ι<VAR>h₁ : i.1 ≤ j<VAR>h₂ : i.2 ≤ j<GOAL>∃ i', f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
<VAR>x : ℝ*<GOAL>x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>J : Type<VAR>inst✝¹ : Fintype J<VAR>f : J → C<VAR>inst✝ : HasBiproduct f<VAR>T : C<VAR>g : (j : J) → f j ⟶ T<VAR>j : J<GOAL>ι f j ≫ desc g = ι f j ≫ ∑ j : J, π f j ≫ g j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>(1 - X ^ 2) * U R n = X * T R (n + 1) - T R (n + 2)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>AEMeasurable (fun b => ⨆ i, f i b) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : BorelSpace α<VAR>inst✝⁷ : TopologicalSpace β<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : BorelSpace β<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : ConditionallyCompleteLinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : SecondCountableTopology α<VAR>ι : Sort u_5<VAR>μ : Measure δ<VAR>inst✝ : Countable ι<VAR>f : ι → δ → α<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<GOAL>(fun b => ⨆ i, f i b) =ᶠ[ae μ] fun b => ⨆ i, AEMeasurable.mk (f i) ⋯ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans (PartialEquiv.refl β)).source = e.source
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Mono (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<GOAL>Mono (app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Mono (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<VAR>ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) := homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯<GOAL>Mono (app' φ 1 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Mono (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<VAR>ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) := homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯<GOAL>(ShortComplex.mk ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯) ⋯).Exact
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.Exact<VAR>hR₂' : Mono (R₂.map' 0 1 ⋯ ⋯)<VAR>h₀ : Mono (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 2 ⋯)<VAR>ψ : mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) := homMk₃ (𝟙 ((mk₃ 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).obj' 0 ⋯)) (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯<GOAL>Mono (ShortComplex.mk ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₂ ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₃ 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯) ⋯).g
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>m : M<GOAL>CompleteLattice.IsCompactElement (lieSpan R L {m})
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s : Set M<VAR>m : M<GOAL>∀ (s : Set (LieSubmodule R L M)), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → lieSpan R L {m} ≤ sSup s → ∃ x ∈ s, lieSpan R L {m} ≤ x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s✝ : Set M<VAR>m : M<VAR>s : Set (LieSubmodule R L M)<VAR>hne : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hsup : lieSpan R L {m} ≤ sSup s<GOAL>∃ x ∈ s, lieSpan R L {m} ≤ x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s✝ : Set M<VAR>m : M<VAR>s : Set (LieSubmodule R L M)<VAR>hne : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hsup : m ∈ ↑(sSup s)<GOAL>∃ x ∈ s, lieSpan R L {m} ≤ x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s✝ : Set M<VAR>m : M<VAR>s : Set (LieSubmodule R L M)<VAR>hne : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hsup : m ∈ ↑(sSup s)<GOAL>↑(sSup s) = ⋃ N ∈ s, ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s✝ : Set M<VAR>m : M<VAR>s : Set (LieSubmodule R L M)<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hsup : m ∈ ↑(sSup s)<VAR>hne : Nonempty ↑s<GOAL>↑(sSup s) = ⋃ N ∈ s, ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s✝ : Set M<VAR>m : M<VAR>s : Set (LieSubmodule R L M)<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hsup : m ∈ ↑(sSup s)<VAR>hne : Nonempty ↑s<VAR>this : ↑(⨆ x, ↑↑x) = ⋃ i, ↑↑↑i<GOAL>↑(sSup s) = ⋃ N ∈ s, ↑N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>s✝ : Set M<VAR>m : M<VAR>s : Set (LieSubmodule R L M)<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hsup : m ∈ ↑(sSup s)<VAR>hne : Nonempty ↑s<VAR>this : ↑(⨆ i, ↑i) = ⋃ i ∈ s, ↑i<GOAL>↑(sSup s) = ⋃ N ∈ s, ↑N
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → α<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>s : Set (SeparationQuotient X)<VAR>l : Filter α<GOAL>Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l