ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>inst✝ : Unique I<GOAL>OrthogonalIdempotents e ↔ IsIdempotentElem (e default)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b c a : α<GOAL>Icc a a = {a}
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : Module.End R M<GOAL>∀ᶠ (n : ℕ) in atTop, ⨅ m, range (f ^ m) = range (f ^ n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : Module.End R M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<GOAL>∀ᶠ (n : ℕ) in atTop, ⨅ m, range (f ^ m) = range (f ^ n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : Module.End R M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>l : ℕ<VAR>hl : l ≥ n<VAR>m : ℕ<GOAL>range (f ^ l) ≤ range (f ^ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : Module.End R M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>l : ℕ<VAR>hl : l ≥ n<VAR>m : ℕ<VAR>h : l ≤ m<GOAL>range (f ^ l) ≤ range (f ^ m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : Module.End R M<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)<VAR>l : ℕ<VAR>hl : l ≥ n<VAR>m : ℕ<VAR>h : m < l<GOAL>range (f ^ l) ≤ range (f ^ m)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * evariance X μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<GOAL>∫⁻ (ω : Ω), ↑‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 ∂μ = ∫⁻ (a : Ω), ENNReal.ofReal (c ^ 2) * ↑‖X a - ∫ (x : Ω), X x ∂μ‖₊ ^ 2 ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>↑‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = ENNReal.ofReal (c ^ 2) * ↑‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>↑(‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2) = ↑((c ^ 2).toNNReal * ‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = (c ^ 2).toNNReal * ‖X ω - ∫ (x : Ω), X x ∂μ‖₊ ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = ‖|c| * (X ω - ∫ (x : Ω), X x ∂μ)‖₊ ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖₊ ^ 2 = ‖c * X ω - c * ∫ (x : Ω), X x ∂μ‖₊ ^ 2
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>∫ (x : Ω), c * X x ∂μ = c * ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ✝ : Measure Ω<VAR>c : ℝ<VAR>X : Ω → ℝ<VAR>μ : Measure Ω<VAR>ω : Ω<GOAL>∫ (x : Ω), c * X x ∂μ = (∫ (x : Ω), X x ∂μ) * c
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>x : F<GOAL>x ∈ ⇑eL ⁻¹' Set.Icc (eL a) (eL b) ↔ x ∈ Set.Icc a b
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<GOAL>Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<VAR>hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b<GOAL>∫ (x : F) in Set.Icc a b, ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i)) = ∫ (x : Fin (n + 1) → ℝ) in Set.Icc (eL a) (eL b), ∑ i : Fin (n + 1), (f' i (eL.symm x)) (eL.symm (e i))
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<VAR>hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b<GOAL>∫ (x : F) in Set.Icc a b, ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i)) = ∫ (x : F) in ⇑eL ⁻¹' Set.Icc (eL a) (eL b), ∑ i : Fin (n + 1), (f' i (eL.symm (eL x))) (eL.symm (e i))
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<VAR>hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b<GOAL>∫ (x : Fin (n + 1) → ℝ) in Set.Icc (eL a) (eL b), ∑ i : Fin (n + 1), (f' i (eL.symm x)) (eL.symm (e i)) = ∑ i : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm (i.insertNth (eL b i) x))) - ∫ (x : Fin n → ℝ) in Set.Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove), f i (eL.symm (i.insertNth (eL a i) x)))
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<VAR>hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b<GOAL>∀ (i : Fin (n + 1)), ContinuousOn ((fun i x => f i (eL.symm x)) i) (Set.Icc (eL a) (eL b))
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<VAR>hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b<GOAL>∀ x ∈ (Set.univ.pi fun i => Set.Ioo (eL a i) (eL b i)) \ ⇑eL.symm ⁻¹' s, ∀ (i : Fin (n + 1)), HasFDerivAt ((fun i x => f i (eL.symm x)) i) ((fun i x => (f' i (eL.symm x)).comp ↑eL.symm) i x) x
<VAR>E : Type u<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>n : ℕ<VAR>F : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : PartialOrder F<VAR>inst✝¹ : MeasureSpace F<VAR>inst✝ : BorelSpace F<VAR>eL : F ≃L[ℝ] Fin (n + 1) → ℝ<VAR>he_ord : ∀ (x y : F), eL x ≤ eL y ↔ x ≤ y<VAR>he_vol : MeasurePreserving (⇑eL) volume volume<VAR>f : Fin (n + 1) → F → E<VAR>f' : Fin (n + 1) → F → F →L[ℝ] E<VAR>s : Set F<VAR>hs : s.Countable<VAR>a b : F<VAR>hle : a ≤ b<VAR>Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)<VAR>Hd : ∀ x ∈ interior (Set.Icc a b) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x<VAR>DF : F → E<VAR>hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), (f' i x) (eL.symm (e i))<VAR>Hi : IntegrableOn DF (Set.Icc a b) volume<VAR>he_emb : MeasurableEmbedding ⇑eL<VAR>hIcc : ⇑eL ⁻¹' Set.Icc (eL a) (eL b) = Set.Icc a b<VAR>hIcc' : Set.Icc (eL a) (eL b) = ⇑eL.symm ⁻¹' Set.Icc a b<GOAL>IntegrableOn (fun x => ∑ i : Fin (n + 1), ((fun i x => (f' i (eL.symm x)).comp ↑eL.symm) i x) (e i)) (Set.Icc (eL a) (eL b)) volume
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<GOAL>P.toPoly = C P.c * X + C P.d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>hs : s₁ = s₂<VAR>ht : ∀ a ∈ s₁, t₁ a = t₂ a<VAR>x : β<GOAL>x ∈ s₁.biUnion t₁ ↔ x ∈ s₂.biUnion t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>hs : s₁ = s₂<VAR>ht : ∀ a ∈ s₁, t₁ a = t₂ a<VAR>x : β<GOAL>(∃ a ∈ s₁, x ∈ t₁ a) ↔ ∃ a ∈ s₂, x ∈ t₂ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>hs : s₁ = s₂<VAR>ht : ∀ a ∈ s₁, t₁ a = t₂ a<VAR>x : β<GOAL>∀ (a : α), a ∈ s₁ ∧ x ∈ t₁ a ↔ a ∈ s₂ ∧ x ∈ t₂ a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>∏ i ∈ ∅, (f i)! ∣ (∑ i ∈ ∅, f i)!
<VAR>α : Type u_1<VAR>s✝ : Finset α<VAR>f : α → ℕ<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : ∏ i ∈ s, (f i)! ∣ (∑ i ∈ s, f i)!<GOAL>∏ i ∈ cons a s has, (f i)! ∣ (∑ i ∈ cons a s has, f i)!
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : PseudoMetrizableSpace β<VAR>fltr : Filter γ<VAR>inst✝¹ : fltr.NeBot<VAR>inst✝ : fltr.IsCountablyGenerated<VAR>U : γ → ι → Ω → β<VAR>h : ∀ (l : γ), ProgMeasurable f (U l)<VAR>h_tendsto : Tendsto U fltr (𝓝 u)<VAR>i : ι<GOAL>StronglyMeasurable fun p => u (↑p.1) p.2
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : PseudoMetrizableSpace β<VAR>fltr : Filter γ<VAR>inst✝¹ : fltr.NeBot<VAR>inst✝ : fltr.IsCountablyGenerated<VAR>U : γ → ι → Ω → β<VAR>h : ∀ (l : γ), ProgMeasurable f (U l)<VAR>h_tendsto : Tendsto U fltr (𝓝 u)<VAR>i : ι<GOAL>Tendsto (fun l p => U l (↑p.1) p.2) fltr (𝓝 fun p => u (↑p.1) p.2)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : PseudoMetrizableSpace β<VAR>fltr : Filter γ<VAR>inst✝¹ : fltr.NeBot<VAR>inst✝ : fltr.IsCountablyGenerated<VAR>U : γ → ι → Ω → β<VAR>h : ∀ (l : γ), ProgMeasurable f (U l)<VAR>h_tendsto : ∀ (x : ι), Tendsto (fun i => U i x) fltr (𝓝 (u x))<VAR>i : ι<GOAL>∀ (x : ↑(Set.Iic i) × Ω), Tendsto (fun i_1 => U i_1 (↑x.1) x.2) fltr (𝓝 (u (↑x.1) x.2))
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : PseudoMetrizableSpace β<VAR>fltr : Filter γ<VAR>inst✝¹ : fltr.NeBot<VAR>inst✝ : fltr.IsCountablyGenerated<VAR>U : γ → ι → Ω → β<VAR>h : ∀ (l : γ), ProgMeasurable f (U l)<VAR>i : ι<VAR>x : ↑(Set.Iic i) × Ω<VAR>h_tendsto : Tendsto (fun i_1 => U i_1 ↑x.1) fltr (𝓝 (u ↑x.1))<GOAL>Tendsto (fun i_1 => U i_1 (↑x.1) x.2) fltr (𝓝 (u (↑x.1) x.2))
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder ι<VAR>u v : ι → Ω → β<VAR>f : Filtration ι m<VAR>γ : Type u_4<VAR>inst✝³ : MeasurableSpace ι<VAR>inst✝² : PseudoMetrizableSpace β<VAR>fltr : Filter γ<VAR>inst✝¹ : fltr.NeBot<VAR>inst✝ : fltr.IsCountablyGenerated<VAR>U : γ → ι → Ω → β<VAR>h : ∀ (l : γ), ProgMeasurable f (U l)<VAR>i : ι<VAR>x : ↑(Set.Iic i) × Ω<VAR>h_tendsto : ∀ (s : Set (Ω → β)), IsOpen s → u ↑x.1 ∈ s → (fun i_1 => U i_1 ↑x.1) ⁻¹' s ∈ fltr<GOAL>∀ (s : Set β), IsOpen s → u (↑x.1) x.2 ∈ s → (fun i_1 => U i_1 (↑x.1) x.2) ⁻¹' s ∈ fltr
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Ring T<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Algebra S T<VAR>inst✝⁵ : Algebra R T<VAR>inst✝⁴ : IsScalarTower R S T<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>b : Basis m R S<VAR>c : Basis n S T<VAR>x : S<VAR>i j : m<VAR>k : n<GOAL>(leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k) = (leftMulMatrix b) x i j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>S : F →L[𝕜] E<GOAL>((adjoint S).comp (T.comp S)).IsPositive
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace F<VAR>T : E →L[𝕜] E<VAR>hT : T.IsPositive<VAR>S : F →L[𝕜] E<GOAL>S = adjoint (adjoint S)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G H I : C ⥤ D<VAR>α : F ⟶ G<VAR>inst✝ : ∀ (X : C), Epi (α.app X)<VAR>Z✝ : C ⥤ D<VAR>g h : G ⟶ Z✝<VAR>eq : α ≫ g = α ≫ h<VAR>X : C<GOAL>g.app X = h.app X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝³ : Monoid M<VAR>inst✝² : LinearOrder M<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h : (map f l).prod < (map g l).prod<GOAL>∃ i ∈ l, f i < g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝³ : Monoid M<VAR>inst✝² : LinearOrder M<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>l : List ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ l, g i ≤ f i<GOAL>(map g l).prod ≤ (map f l).prod
<VAR>α : Type u<VAR>c d : Cardinal.{u}<GOAL>StrictMonoOn (⇑toNat) (Iio ℵ₀)
<VAR>α : Type u<VAR>c d : Cardinal.{u}<GOAL>∀ (i i_1 : ℕ), i < i_1 → i < i_1
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>y : L'<VAR>h₁ : Function.Surjective ⇑f<VAR>h₂ : y ∈ map f I<GOAL>∃ x, f ↑x = y
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>y : L'<VAR>h₁ : Function.Surjective ⇑f<VAR>h₂ : ∃ y_1 ∈ ↑I, ↑f y_1 = y<GOAL>∃ x, f ↑x = y
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h₁ : Function.Surjective ⇑f<VAR>x : L<VAR>hx : x ∈ ↑I<GOAL>∃ x_1, f ↑x_1 = ↑f x
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<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>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h₁ : Function.Surjective ⇑f<VAR>x : L<VAR>hx : x ∈ ↑I<GOAL>f ↑⟨x, hx⟩ = ↑f x
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>R : Type u_1<VAR>r : K<VAR>x : FractionRing K[X]<GOAL>r • { toFractionRing := x } = Polynomial.C r • { toFractionRing := x }
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>R : Type u_1<VAR>r : K<VAR>y✝ : K[X] × ↥K[X]⁰<GOAL>r • { toFractionRing := Localization.mk y✝.1 y✝.2 } = Polynomial.C r • { toFractionRing := Localization.mk y✝.1 y✝.2 }
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>H : SimpleGraph V<VAR>a b : Fin n<GOAL>(turanGraph n 0).Adj a b ↔ ⊤.Adj a b
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>i : E →ₐ[F] K<VAR>x : E<GOAL>x ∈ comap i (perfectClosure F K) ↔ x ∈ perfectClosure F E
<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<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<GOAL>DifferentiableAt 𝕜 (f ∘ ⇑iso) x ↔ DifferentiableAt 𝕜 f (iso x)
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.prod ν) (s ×ˢ t) = μ s * ν t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<VAR>h : r.codom ⊆ s<GOAL>r.preimage s = r.dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<VAR>h : r.codom ⊆ s<GOAL>r.preimage s = r.preimage Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<VAR>h : r.codom ⊆ s<GOAL>r.preimage s ⊆ r.preimage Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set β<VAR>h : r.codom ⊆ s<GOAL>r.preimage Set.univ ⊆ r.preimage s