ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<VAR>i : ι<VAR>j : ι<VAR>hj : j ≤ i<GOAL>MeasurableSet (s j)
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>s : ι → Set Ω<VAR>hsm : ∀ (n : ι), MeasurableSet (s n)<VAR>i : ι<GOAL>MeasurableSet (s i)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>TopologicalSpace β<VAR>TopologicalSpace.MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>BorelSpace β<VAR>Preorder ι<VAR>MulZeroOneClass β<VAR>Nontrivial β<VAR>s : ι → Set Ω<VAR>hsm : ∀ (i : ι), MeasurableSet (s i)<GOAL>MeasureTheory.filtrationOfSet hsm = MeasureTheory.Filtration.natural (fun i => (s i).indicator fun x => 1) ⋯
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>E : Type u_4<VAR>Zero E<VAR>TopologicalSpace E<VAR>ℱ : MeasureTheory.Filtration ι m<VAR>f : ι → Ω → E<VAR>μ : MeasureTheory.Measure Ω<GOAL>MeasureTheory.StronglyMeasurable (MeasureTheory.Filtration.limitProcess f ℱ μ)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>μ : MeasureTheory.Measure Ω<VAR>R : ℝ≥0<VAR>p : ℝ≥0∞<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>ℱ : MeasureTheory.Filtration ℕ m<VAR>f : ℕ → Ω → F<VAR>hfm : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ<VAR>hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R<GOAL>MeasureTheory.Memℒp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ
<VAR>f g : ℝ → ℝ<VAR>hfg : f =ᶠ[Filter.atTop] g<VAR>hg : AkraBazziRecurrence.GrowsPolynomially g<GOAL>AkraBazziRecurrence.GrowsPolynomially f
<VAR>f g : ℝ → ℝ<VAR>h : f =ᶠ[Filter.atTop] g<GOAL>AkraBazziRecurrence.GrowsPolynomially f ↔ AkraBazziRecurrence.GrowsPolynomially g
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u
<VAR>f : ℝ → ℝ<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hf' : ∃ᶠ (x : ℝ) in Filter.atTop, f x = 0<GOAL>∀ᶠ (x : ℝ) in Filter.atTop, f x = 0
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>(∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in Filter.atTop, f x ≤ 0
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>(∀ᶠ (x : ℝ) in Filter.atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in Filter.atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in Filter.atTop, f x < 0
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>AkraBazziRecurrence.GrowsPolynomially (-f)
<VAR>f : ℝ → ℝ<GOAL>AkraBazziRecurrence.GrowsPolynomially f ↔ AkraBazziRecurrence.GrowsPolynomially (-f)
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => |f x|
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => ‖f x‖
<VAR>c : ℝ<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => c
<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => x
<VAR>f g : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hg : AkraBazziRecurrence.GrowsPolynomially g<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x * g x
<VAR>f : ℝ → ℝ<VAR>c : ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => c * f x
<VAR>f g : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hg : AkraBazziRecurrence.GrowsPolynomially g<VAR>hf' : 0 ≤ᶠ[Filter.atTop] f<VAR>hg' : 0 ≤ᶠ[Filter.atTop] g<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x + g x
<VAR>f g : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hfg : g =o[Filter.atTop] f<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x + g x
<VAR>f : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => (f x)⁻¹
<VAR>f g : ℝ → ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hg : AkraBazziRecurrence.GrowsPolynomially g<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x / g x
<VAR>f : ℝ → ℝ<VAR>p : ℝ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
<VAR>f : ℝ → ℝ<VAR>p : ℕ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
<VAR>f : ℝ → ℝ<VAR>p : ℤ<VAR>hf : AkraBazziRecurrence.GrowsPolynomially f<VAR>hf_nonneg : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
<VAR>p : ℝ<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => x ^ p
<VAR>p : ℕ<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => x ^ p
<VAR>p : ℤ<GOAL>AkraBazziRecurrence.GrowsPolynomially fun x => x ^ p
<GOAL>AkraBazziRecurrence.GrowsPolynomially Real.log
<VAR>f g : ℝ → ℝ<VAR>hg : AkraBazziRecurrence.GrowsPolynomially g<VAR>hf : f =Θ[Filter.atTop] g<VAR>hf' : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x<GOAL>AkraBazziRecurrence.GrowsPolynomially f
<VAR>f g : ℝ → ℝ<VAR>hg : AkraBazziRecurrence.GrowsPolynomially g<VAR>hf : f ~[Filter.atTop] g<GOAL>AkraBazziRecurrence.GrowsPolynomially f
<VAR>f : ℝ → ℝ<VAR>c : ℝ<VAR>hf : f ~[Filter.atTop] fun x => c<GOAL>AkraBazziRecurrence.GrowsPolynomially f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hf : ¬Measurable (Function.uncurry f)<GOAL>κ.withDensity f = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<GOAL>(κ.withDensity f) a = (κ a).withDensity (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<VAR>s : Set β<GOAL>((κ.withDensity f) a) s = ∫⁻ (b : β) in s, f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), f a =ᵐ[κ a] g a<GOAL>κ.withDensity f = κ.withDensity g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0∞<VAR>a : α<GOAL>(κ.withDensity f) a ≪ κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>κ.withDensity 1 = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>(κ.withDensity fun x x => 1) = κ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>κ.withDensity 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<GOAL>(κ.withDensity fun x x => 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<VAR>g : β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (b : β), g b ∂(κ.withDensity f) a = ∫⁻ (b : β), f a b * g b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : β → E<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>a : α<VAR>g : α → β → ℝ≥0<VAR>hg : Measurable (Function.uncurry g)<GOAL>∫ (b : β), f b ∂(κ.withDensity fun a b => ↑(g a b)) a = ∫ (b : β), g a b • f b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>ProbabilityTheory.IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<GOAL>(κ + η).withDensity f = κ.withDensity f + η.withDensity f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κ : ι → ProbabilityTheory.Kernel α β<VAR>hκ : ∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i)<VAR>f : α → β → ℝ≥0∞<GOAL>(ProbabilityTheory.Kernel.sum κ).withDensity f = ProbabilityTheory.Kernel.sum fun i => (κ i).withDensity f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<GOAL>κ.withDensity (f + g) = κ.withDensity f + κ.withDensity g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<VAR>hfg : ∀ (a : α), g a ≤ᵐ[κ a] f a<GOAL>(κ.withDensity fun a x => f a x - g a x) + κ.withDensity g = κ.withDensity f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>Countable ι<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : ι → α → β → ℝ≥0∞<VAR>hf : ∀ (i : ι), Measurable (Function.uncurry (f i))<GOAL>κ.withDensity (∑' (n : ι), f n) = ProbabilityTheory.Kernel.sum fun n => κ.withDensity (f n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>B : ℝ≥0∞<VAR>hB_top : B ≠ ⊤<VAR>hf_B : ∀ (a : α) (b : β), f a b ≤ B<GOAL>ProbabilityTheory.IsFiniteKernel (κ.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<GOAL>ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β → ℝ≥0∞<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<GOAL>ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : ProbabilityTheory.Kernel α β<VAR>ProbabilityTheory.IsSFiniteKernel κ<VAR>f : α → β → ℝ≥0<VAR>g : α → β → ℝ≥0∞<VAR>hf : Measurable (Function.uncurry f)<VAR>hg : Measurable (Function.uncurry g)<GOAL>(κ.withDensity fun a x => ↑(f a x) * g a x) = (κ.withDensity fun a x => ↑(f a x)).withDensity g
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.mongePoint = (↑(n + 1) / ↑(n - 1)) • (Finset.centroid ℝ Finset.univ s.points -ᵥ s.circumcenter) +ᵥ s.circumcenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P n<GOAL>s.mongePoint ∈ affineSpan ℝ (Set.range s.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s₁ s₂ : Affine.Simplex ℝ P n<VAR>h : Set.range s₁.points = Set.range s₂.points<GOAL>s₁.mongePoint = s₂.mongePoint
<VAR>n : ℕ<GOAL>∑ i : Affine.Simplex.PointsWithCircumcenterIndex (n + 2), Affine.Simplex.mongePointWeightsWithCircumcenter n i = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<GOAL>s.mongePoint = (Finset.affineCombination ℝ Finset.univ s.pointsWithCircumcenter) (Affine.Simplex.mongePointWeightsWithCircumcenter n)
<VAR>n : ℕ<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ = Affine.Simplex.mongePointWeightsWithCircumcenter n - Affine.Simplex.centroidWeightsWithCircumcenter {i₁, i₂}ᶜ
<VAR>n : ℕ<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>∑ i : Affine.Simplex.PointsWithCircumcenterIndex (n + 2), Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂ i = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<VAR>h : i₁ ≠ i₂<GOAL>s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points = (Finset.univ.weightedVSub s.pointsWithCircumcenter) (Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>s.mongePlane i₁ i₂ = AffineSubspace.mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ affineSpan ℝ (Set.range s.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>s.mongePlane i₁ i₂ = s.mongePlane i₂ i₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>s.mongePoint ∈ s.mongePlane i₁ i₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>(s.mongePlane i₁ i₂).direction = (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 2)<VAR>i₁ : Fin (n + 3)<VAR>p : P<VAR>h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂<GOAL>p = s.mongePoint
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>s.altitude i = AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>s.points i ∈ s.altitude i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>(s.altitude i).direction = (vectorSpan ℝ (s.points '' ↑(Finset.univ.erase i)))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>vectorSpan ℝ (s.points '' ↑(Finset.univ.erase i)) ⟂ (s.altitude i).direction
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<GOAL>FiniteDimensional.finrank ℝ ↥(s.altitude i).direction = 1
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Affine.Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<VAR>p : P<GOAL>affineSpan ℝ {p, s.points i} = s.altitude i ↔ p ≠ s.points i ∧ p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).directionᗮ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<GOAL>t.orthocenter = Affine.Simplex.mongePoint t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<GOAL>t.orthocenter = 3 • (Finset.centroid ℝ Finset.univ t.points -ᵥ Affine.Simplex.circumcenter t) +ᵥ Affine.Simplex.circumcenter t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<GOAL>t.orthocenter ∈ affineSpan ℝ (Set.range t.points)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t₁ t₂ : Affine.Triangle ℝ P<VAR>h : Set.range t₁.points = Set.range t₂.points<GOAL>t₁.orthocenter = t₂.orthocenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>Affine.Simplex.altitude t i₁ = Affine.Simplex.mongePlane t i₂ i₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>i₁ : Fin 3<GOAL>t.orthocenter ∈ Affine.Simplex.altitude t i₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>p : P<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁ : p ∈ Affine.Simplex.altitude t i₁<VAR>h₂ : p ∈ Affine.Simplex.altitude t i₂<GOAL>p = t.orthocenter
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<GOAL>dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' {i₁, i₂}))) (Affine.Simplex.circumcenter t)) = Affine.Simplex.circumradius t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<GOAL>dist t.orthocenter ((EuclideanGeometry.reflection (affineSpan ℝ (t.points '' ↑{i₁, i₂}))) (Affine.Simplex.circumcenter t)) = Affine.Simplex.circumradius t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>i : Fin 3<GOAL>affineSpan ℝ {t.orthocenter, t.points i} ≤ Affine.Simplex.altitude t i
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t₁ t₂ : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>Affine.Simplex.altitude t₂ j₂ = affineSpan ℝ {t₁.points i₁, t₁.points i₂}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t₁ t₂ : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ j₁ j₂ j₃ : Fin 3<VAR>hi₁₂ : i₁ ≠ i₂<VAR>hi₁₃ : i₁ ≠ i₃<VAR>hi₂₃ : i₂ ≠ i₃<VAR>hj₁₂ : j₁ ≠ j₂<VAR>hj₁₃ : j₁ ≠ j₃<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₁ : t₂.points j₁ = t₁.orthocenter<VAR>h₂ : t₂.points j₂ = t₁.points i₂<VAR>h₃ : t₂.points j₃ = t₁.points i₃<GOAL>t₂.orthocenter = t₁.points i₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>ho : t.orthocenter ∉ Set.range t.points<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hpi : Function.Injective p<GOAL>(∃ i₁ i₂ i₃ j₂ j₃, i₁ ≠ i₂ ∧ i₁ ≠ i₃ ∧ i₂ ≠ i₃ ∧ (∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃) ∧ p i₁ = t.orthocenter ∧ j₂ ≠ j₃ ∧ t.points j₂ = p i₂ ∧ t.points j₃ = p i₃) ∨ Set.range p = Set.range t.points
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>t : Affine.Triangle ℝ P<VAR>ho : t.orthocenter ∉ Set.range t.points<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hpi : Function.Injective p<GOAL>∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Affine.Simplex.circumradius t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<VAR>ho : EuclideanGeometry.OrthocentricSystem s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<GOAL>AffineIndependent ℝ p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<VAR>ho : EuclideanGeometry.OrthocentricSystem s<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ s<VAR>hpi : Function.Injective p<GOAL>affineSpan ℝ (Set.range p) = affineSpan ℝ s
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<VAR>ho : EuclideanGeometry.OrthocentricSystem s<GOAL>∃ r, ∀ (t : Affine.Triangle ℝ P), Set.range t.points ⊆ s → Affine.Simplex.circumradius t = r
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s : Set P<VAR>ho : EuclideanGeometry.OrthocentricSystem s<VAR>t : Affine.Triangle ℝ P<VAR>ht : Set.range t.points ⊆ s<GOAL>s = insert t.orthocenter (Set.range t.points)
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : List Γ<GOAL>Turing.BlankExtends l l
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l₁ l₂ l₃ : List Γ<GOAL>Turing.BlankExtends l₁ l₂ → Turing.BlankExtends l₂ l₃ → Turing.BlankExtends l₁ l₃
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l l₁ l₂ : List Γ<GOAL>Turing.BlankExtends l l₁ → Turing.BlankExtends l l₂ → l₁.length ≤ l₂.length → Turing.BlankExtends l₁ l₂
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l l₁ l₂ : List Γ<GOAL>Turing.BlankExtends l₁ l → Turing.BlankExtends l₂ l → l₁.length ≤ l₂.length → Turing.BlankExtends l₁ l₂
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : List Γ<GOAL>Turing.BlankRel l l
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l₁ l₂ : List Γ<GOAL>Turing.BlankRel l₁ l₂ → Turing.BlankRel l₂ l₁
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l₁ l₂ l₃ : List Γ<GOAL>Turing.BlankRel l₁ l₂ → Turing.BlankRel l₂ l₃ → Turing.BlankRel l₁ l₃
<VAR>Γ : Type u_1<VAR>Inhabited Γ<GOAL>Equivalence Turing.BlankRel
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>p : Turing.ListBlank Γ → Prop<VAR>q : Turing.ListBlank Γ<VAR>h : ∀ (a : List Γ), p (Turing.ListBlank.mk a)<GOAL>p q
<VAR>Γ : Type u_1<VAR>Inhabited Γ<VAR>l : List Γ<GOAL>(Turing.ListBlank.mk l).head = l.headI