ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hai : AffineIndependent k (⇑f ∘ p)<VAR>i : ι<GOAL>LinearIndependent k fun i_1 => p ↑i_1 -ᵥ p i
<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>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>i : ι<VAR>hai : LinearIndependent k fun i_1 => f.linear (p ↑i_1 -ᵥ p i)<GOAL>LinearIndependent k fun i_1 => p ↑i_1 -ᵥ p i
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>h₁ : π₁.IsPartition<VAR>h₂ : π₂.IsPartition<GOAL>(π₁ ⊓ π₂).iUnion = ↑I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>g : ι → α → E := fun i => Exists.choose ⋯<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>g : ι → α → E := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>g : ι → α → E := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<GOAL>UniformIntegrable f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>E : Type u_5<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>ι : Type u_6<VAR>f : ι → α → E<VAR>j : ι<VAR>p : ℝ≥0∞<VAR>hp : 1 ≤ p<VAR>hp' : p ≠ ⊤<VAR>hℒp : Memℒp (f j) p μ<VAR>hf : ∀ (i : ι), IdentDistrib (f i) (f j) μ μ<VAR>hfmeas : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>g : ι → α → E := fun i => Exists.choose ⋯<VAR>hgmeas : ∀ (i : ι), StronglyMeasurable (g i)<VAR>hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i<VAR>hgℒp : Memℒp (g j) p μ<GOAL>UniformIntegrable f p μ
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>f : X →ᵇ ℝ<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) ⊥<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) ⊥ (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i) _auto✝
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i) _auto✝
<VAR>Ω : Type u_1<VAR>F : Type u_2<VAR>m mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>ω : Ω<GOAL>(condexpKernel μ m) ω = (condDistrib id id μ) (id ω)
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → ProbabilityMeasure Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → ProbabilityMeasure Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>Tendsto (toFiniteMeasure ∘ μs) F (𝓝 μ.toFiniteMeasure) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → ProbabilityMeasure Ω<VAR>μ : ProbabilityMeasure Ω<GOAL>(∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (x : Ω), f x ∂↑((toFiniteMeasure ∘ μs) i)) F (𝓝 (∫ (x : Ω), f x ∂↑μ.toFiniteMeasure))) ↔ ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), f ω ∂↑μ))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<GOAL>finrank K V = 1 ↔ ∃ v, v ≠ 0 ∧ ∀ (w : V), ∃ c, c • v = w
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module.Free K V<GOAL>finrank K V = 1 ↔ Module.rank K V = 1
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype p<VAR>inst✝ : Fintype q<VAR>i : R<VAR>hi : i * i = -1<VAR>A : ↥(so' p q R)<GOAL>↑((soIndefiniteEquiv p q R hi) A) = (Pso p q R i)⁻¹ * ↑A * Pso p q R i
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁶ : DecidableEq n<VAR>inst✝⁵ : DecidableEq p<VAR>inst✝⁴ : DecidableEq q<VAR>inst✝³ : DecidableEq l<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype p<VAR>inst✝ : Fintype q<VAR>i : R<VAR>hi : i * i = -1<VAR>A : ↥(so' p q R)<GOAL>↑((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)) A) = (Pso p q R i)⁻¹ * ↑A * Pso p q R i
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.114338}<VAR>ho : 0 < o<GOAL>0 < type fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>a b : α<VAR>s : α → Set β<GOAL>⋂ x ∈ {a, b}, s x = s a ∩ s b
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>I : Ideal A<VAR>h : I.FG<VAR>inst✝ : FinitePresentation R A<GOAL>∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>I : Ideal A<VAR>h : I.FG<VAR>inst✝ : FinitePresentation R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG<GOAL>∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
<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>inst✝ : CommRing S<VAR>w x y z : S<GOAL>C w * (X - C x) * (X - C y) * (X - C z) = { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly
<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>inst✝ : CommRing S<VAR>w x y z : S<GOAL>C w * (X - C x) * (X - C y) * (X - C z) = C w * X ^ 3 + C w * -(C x + C y + C z) * X ^ 2 + C w * (C x * C y + C x * C z + C y * C z) * X + C w * -(C x * C y * C z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s t : Set α<VAR>a : α<VAR>h : IsLowerSet sᶜ<GOAL>IsUpperSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s t : Set α<VAR>a : α<VAR>h : IsLowerSet sᶜ<GOAL>s = sᶜᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>t : Set α<GOAL>(ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(Multiset.card s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>t : Set α<GOAL>∑' (x : α), t.indicator (⇑(ofMultiset s hs)) x = ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑(Multiset.card s))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Multiset α<VAR>hs : s ≠ 0<VAR>t : Set α<VAR>x : α<GOAL>t.indicator (⇑(ofMultiset s hs)) x = ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(Multiset.card s))⁻¹
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>((s • M).updateColumn j u).det = s ^ (Fintype.card n - 1) * (M.updateColumn j u).det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateColumn j u).det
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Ioi x) x<GOAL>slope f x y < f'
<VAR>S : Type u_1<VAR>inst✝ : UnitalShelf S<VAR>x : S<GOAL>x ◃ x = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Icc a b = cons b (Ico a b) ⋯
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>∠ p₁ p₂ p₃ = π ↔ Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>∠ p₁ p₂ p₃ = π → Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<GOAL>(p₁ -ᵥ p₂ ≠ 0 ∧ ∃ r < 0, p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)) → Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ -ᵥ p₂ ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)<GOAL>Sbtw ℝ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ -ᵥ p₂ ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)<GOAL>(AffineMap.lineMap p₁ p₃) (1 / (1 - r)) = p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁✝ p₂✝ p₁ p₂ p₃ : P<VAR>hp₁p₂ : p₁ -ᵥ p₂ ≠ 0<VAR>r : ℝ<VAR>hr : r < 0<VAR>hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)<GOAL>p₂ ≠ p₃
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivAt f f' x<VAR>hx : f x ≠ 0<GOAL>HasDerivAt (fun y => Real.log (f y)) (f' / f x) x
<VAR>f : ℝ → ℝ<VAR>x f' : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' Set.univ x<VAR>hx : f x ≠ 0<GOAL>HasDerivWithinAt (fun y => Real.log (f y)) (f' / f x) Set.univ x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>v : Set E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ (span 𝕜 v)ᗮ = ⊥
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>v : Set E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>h : IdentDistrib f g μ ν<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>μ (f ⁻¹' s) = ν (g ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<GOAL>e.det ⇑e = 1
<VAR>X✝ Y✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>hU✝ : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X✝, U✝)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>r : ↑Γ(Y, U)<GOAL>Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((Scheme.Hom.appLE f U V e) r)) ⋯ = IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r)) (↑Γ(X, X.basicOpen ((Scheme.Hom.appLE f U V e) r))) (Scheme.Hom.appLE f U V e) r
<VAR>X✝ Y✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>hU✝ : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X✝, U✝)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>r : ↑Γ(Y, U)<VAR>this : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r<GOAL>Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((Scheme.Hom.appLE f U V e) r)) ⋯ = IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r)) (↑Γ(X, X.basicOpen ((Scheme.Hom.appLE f U V e) r))) (Scheme.Hom.appLE f U V e) r
<VAR>X✝ Y✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>hU✝ : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X✝, U✝)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>r : ↑Γ(Y, U)<VAR>this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r<VAR>this : IsLocalization.Away ((Scheme.Hom.appLE f U V e) r) ↑Γ(X, X.basicOpen ((Scheme.Hom.appLE f U V e) r)) := isLocalization_basicOpen hV ((Scheme.Hom.appLE f U V e) r)<GOAL>Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((Scheme.Hom.appLE f U V e) r)) ⋯ = IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r)) (↑Γ(X, X.basicOpen ((Scheme.Hom.appLE f U V e) r))) (Scheme.Hom.appLE f U V e) r
<VAR>X✝ Y✝ : Scheme<VAR>U✝ : X✝.Opens<VAR>hU✝ : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X✝, U✝)<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : IsAffineOpen U<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>e : V ≤ f ⁻¹ᵁ U<VAR>r : ↑Γ(Y, U)<VAR>this✝ : IsLocalization.Away r ↑Γ(Y, Y.basicOpen r) := isLocalization_basicOpen hU r<VAR>this : IsLocalization.Away ((Scheme.Hom.appLE f U V e) r) ↑Γ(X, X.basicOpen ((Scheme.Hom.appLE f U V e) r)) := isLocalization_basicOpen hV ((Scheme.Hom.appLE f U V e) r)<GOAL>RingHom.comp (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((Scheme.Hom.appLE f U V e) r)) ⋯) (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r)) = (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r)) (↑Γ(X, X.basicOpen ((Scheme.Hom.appLE f U V e) r))) (Scheme.Hom.appLE f U V e) r).comp (algebraMap ↑Γ(Y, U) ↑Γ(Y, Y.basicOpen r))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s✝ t : Set α<VAR>l : List α<VAR>a : α<VAR>f : α → β<VAR>hf : ∀ {x y : α}, x < y ↔ f x < f y<VAR>s : Set α<GOAL>(f '' s).chainHeight = s.chainHeight
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s✝ t : Set α<VAR>l : List α<VAR>a : α<VAR>f : α → β<VAR>hf : ∀ {x y : α}, x < y ↔ f x < f y<VAR>s : Set α<GOAL>∀ l ∈ (f '' s).subchain, ∃ l' ∈ s.subchain, l.length = l'.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s✝ t : Set α<VAR>l : List α<VAR>a : α<VAR>f : α → β<VAR>hf : ∀ {x y : α}, x < y ↔ f x < f y<VAR>s : Set α<GOAL>∀ l ∈ s.subchain, ∃ l' ∈ (f '' s).subchain, l.length = l'.length
<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>j : ℤ<GOAL>stdAddChar ↑j = cexp (2 * ↑π * I * ↑j / ↑N)