ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E✝ : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι✝ : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜✝<VAR>inst✝⁶ : AddCommGroup E✝<VAR>inst✝⁵ : Module 𝕜✝ E✝<VAR>p✝ : SeminormFamily 𝕜✝ E✝ ι✝<VAR>inst✝⁴ : Nonempty ι✝<VAR>𝕜 : Type u_10<VAR>E : Type u_11<VAR>ι : Type u_12<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>U ∈ 𝓝 0
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E✝ : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι✝ : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜✝<VAR>inst✝⁶ : AddCommGroup E✝<VAR>inst✝⁵ : Module 𝕜✝ E✝<VAR>p✝ : SeminormFamily 𝕜✝ E✝ ι✝<VAR>inst✝⁴ : Nonempty ι✝<VAR>𝕜 : Type u_10<VAR>E : Type u_11<VAR>ι : Type u_12<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : (s.sup p).ball 0 r ∈ p.basisSets<GOAL>(s.sup p).ball 0 r ∈ 𝓝 0
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E✝ : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι✝ : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜✝<VAR>inst✝⁶ : AddCommGroup E✝<VAR>inst✝⁵ : Module 𝕜✝ E✝<VAR>p✝ : SeminormFamily 𝕜✝ E✝ ι✝<VAR>inst✝⁴ : Nonempty ι✝<VAR>𝕜 : Type u_10<VAR>E : Type u_11<VAR>ι : Type u_12<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(s.sup p).ball 0 r ∈ 𝓝 0
<VAR>𝕜✝ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E✝ : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι✝ : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁷ : NormedField 𝕜✝<VAR>inst✝⁶ : AddCommGroup E✝<VAR>inst✝⁵ : Module 𝕜✝ E✝<VAR>p✝ : SeminormFamily 𝕜✝ E✝ ι✝<VAR>inst✝⁴ : Nonempty ι✝<VAR>𝕜 : Type u_10<VAR>E : Type u_11<VAR>ι : Type u_12<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : ∀ (i : ι), Continuous ⇑(p i)<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>Continuous ⇑(s.sup p)
<VAR>k : Type u_1<VAR>A : Type u_2<VAR>G : Type u_3<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Semiring k<VAR>s : Set G<VAR>x : MonoidAlgebra k G<GOAL>x ∈ Ideal.span (⇑(of k G) '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d * m'
<VAR>k : Type u_1<VAR>A : Type u_2<VAR>G : Type u_3<VAR>inst✝¹ : Monoid G<VAR>inst✝ : Semiring k<VAR>s : Set G<VAR>x : MonoidAlgebra k G<VAR>RHS : Ideal (MonoidAlgebra k G) := { carrier := {p | ∀ m ∈ p.support, ∃ m' ∈ s, ∃ d, m = d * m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<GOAL>x ∈ Ideal.span (⇑(of k G) '' s) ↔ ∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d * m'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ a * b ↔ a * 1 ≤ a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<GOAL>UnifTight f p μ ↔ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hut : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hut : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ((fun a => ↑a) ε)<GOAL>∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hut : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ((fun a => ↑a) ε)<GOAL>∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f✝ g : ι → α → β<VAR>p✝ : ℝ≥0∞<VAR>x✝ : MeasurableSpace α<VAR>f : ι → α → β<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>hut : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ε<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>hfε : ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ENNReal.ofReal ((fun a => ↑a) ε)<VAR>i : ι<GOAL>eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α✝<VAR>inst✝³ : MeasurableSpace β✝<VAR>μ✝ ν ν₁ ν₂ : Measure α✝<VAR>s t : Set α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>g : α → β<VAR>g_mble : NullMeasurable g μ<GOAL>{t | 0 < μ {a | g a = t}}.Countable
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α✝<VAR>inst✝³ : MeasurableSpace β✝<VAR>μ✝ ν ν₁ ν₂ : Measure α✝<VAR>s t : Set α✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass β<VAR>g : α → β<VAR>g_mble : NullMeasurable g μ<VAR>level_sets_disjoint : Pairwise (Disjoint on fun t => {a | g a = t})<GOAL>{t | 0 < μ {a | g a = t}}.Countable
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>hx : x₁ = x₂<VAR>hy : y₁ ≠ W.negY x₂ y₂<GOAL>W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I M : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hIM : I ≤ M<VAR>hM : M.IsMaximal<GOAL>∃ Z, (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I M : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hIM : I ≤ M<VAR>hM : M.IsMaximal<VAR>Z₀ : Multiset (PrimeSpectrum A)<VAR>hZ₀ : (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≠ ⊥<GOAL>∃ Z, (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I M : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hIM : I ≤ M<VAR>hM : M.IsMaximal<VAR>Z₀ : Multiset (PrimeSpectrum A)<VAR>hZ₀ : (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≠ ⊥<VAR>Z : Multiset (PrimeSpectrum A)<VAR>h_eraseZ : ∀ x ∈ {Z | (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥}, ¬x < Z<VAR>hZI : (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I<VAR>hprodZ : (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥<GOAL>∃ Z, (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I M : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hIM : I ≤ M<VAR>hM : M.IsMaximal<VAR>Z₀ : Multiset (PrimeSpectrum A)<VAR>hZ₀ : (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≠ ⊥<VAR>Z : Multiset (PrimeSpectrum A)<VAR>h_eraseZ : ∀ x ∈ {Z | (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥}, ¬x < Z<VAR>hZI : (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I<VAR>hprodZ : (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥<VAR>w✝ : Ideal A<VAR>hPZ' : w✝ ∈ Multiset.map PrimeSpectrum.asIdeal Z<VAR>hPM : w✝ ≤ M<GOAL>∃ Z, (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : IsDedekindDomain A<VAR>hNF : ¬IsField A<VAR>I M : Ideal A<VAR>hI0 : I ≠ ⊥<VAR>hIM : I ≤ M<VAR>hM : M.IsMaximal<VAR>Z₀ : Multiset (PrimeSpectrum A)<VAR>hZ₀ : (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z₀).prod ≠ ⊥<VAR>Z : Multiset (PrimeSpectrum A)<VAR>h_eraseZ : ∀ x ∈ {Z | (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥}, ¬x < Z<VAR>hZI : (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I<VAR>hprodZ : (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥<VAR>P : PrimeSpectrum A<VAR>hPZ : P ∈ Z<VAR>hPZ' : P.asIdeal ∈ Multiset.map PrimeSpectrum.asIdeal Z<VAR>hPM : P.asIdeal ≤ M<GOAL>∃ Z, (M ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>a : 𝕜<VAR>h : Tendsto f l (𝓝 a)<VAR>hg : Tendsto g l atTop<GOAL>Tendsto (fun x => f x / g x) l (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>a : 𝕜<VAR>h : Tendsto f l (𝓝 a)<VAR>hg : Tendsto g l atTop<GOAL>Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a < b<VAR>hf_c : ContinuousOn f (Ioo a b)<VAR>hf_i : InjOn f (Ioo a b)<GOAL>StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a < b<VAR>hf_c : ContinuousOn f (Ioo a b)<VAR>hf_i : InjOn f (Ioo a b)<VAR>this : Inhabited ↑(Ioo a b)<GOAL>StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a < b<VAR>hf_c : ContinuousOn f (Ioo a b)<VAR>hf_i : InjOn f (Ioo a b)<VAR>this : Inhabited ↑(Ioo a b)<VAR>g : ↑(Ioo a b) → δ := (Ioo a b).restrict f<GOAL>StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>a b : α<VAR>f : α → δ<VAR>hab : a < b<VAR>hf_c : ContinuousOn f (Ioo a b)<VAR>hf_i : InjOn f (Ioo a b)<VAR>this✝ : Inhabited ↑(Ioo a b)<VAR>g : ↑(Ioo a b) → δ := (Ioo a b).restrict f<VAR>this : StrictMono g ∨ StrictAnti g<GOAL>StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>f✝ : α → β<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : SecondCountableTopology β<VAR>f : α → β<VAR>hf : _root_.Embedding f<GOAL>SeparableSpace α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>f✝ : α → β<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : SecondCountableTopology β<VAR>f : α → β<VAR>hf : _root_.Embedding f<VAR>this : SecondCountableTopology α<GOAL>SeparableSpace α
<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✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hd : M<VAR>tl : List M<VAR>ih : (∀ x ∈ tl, 1 ≤ x) → 1 ≤ tl.prod<VAR>hl₁ : ∀ x ∈ hd :: tl, 1 ≤ x<GOAL>1 ≤ (hd :: tl).prod
<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✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>hd : M<VAR>tl : List M<VAR>ih : (∀ x ∈ tl, 1 ≤ x) → 1 ≤ tl.prod<VAR>hl₁ : ∀ x ∈ hd :: tl, 1 ≤ x<GOAL>1 ≤ hd * tl.prod
<VAR>α : Type u_1<VAR>s✝ t✝ : Finset α<VAR>n✝ : ?m.14976<VAR>s t : Finset α<VAR>n : ℕ<GOAL>(↑(powersetCard n ∅)).Subsingleton
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : ¬λ ∣ x<GOAL>λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : ¬λ ∣ x<VAR>H : λ ∣ x<GOAL>λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : ¬λ ∣ x<VAR>H : λ ∣ x - 1<GOAL>λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>x✝ x : 𝓞 K<VAR>h : ¬λ ∣ x<VAR>H : λ ∣ x + 1<GOAL>λ ^ 4 ∣ x ^ 3 - 1 ∨ λ ^ 4 ∣ x ^ 3 + 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>f : G → E<VAR>s : Set G<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) (f x) < r
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s✝ t✝ : Multiset α<VAR>f✝ g✝ : α → Multiset β<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>f : α → Multiset γ<VAR>g : β → Multiset δ<VAR>h : (r ⇒ Rel p) f g<VAR>hst : Rel r s t<GOAL>Rel p (s.bind f) (t.bind g)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s✝ t✝ : Multiset α<VAR>f✝ g✝ : α → Multiset β<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>f : α → Multiset γ<VAR>g : β → Multiset δ<VAR>h : (r ⇒ Rel p) f g<VAR>hst : Rel r s t<GOAL>Rel (Rel p) (map f s) (map g t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s✝ t✝ : Multiset α<VAR>f✝ g✝ : α → Multiset β<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>s : Multiset α<VAR>t : Multiset β<VAR>f : α → Multiset γ<VAR>g : β → Multiset δ<VAR>h : (r ⇒ Rel p) f g<VAR>hst : Rel r s t<GOAL>Rel (fun a b => Rel p (f a) (g b)) s t
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x y : WithLp 2 (α × β)<GOAL>edist x y = (edist x.1 y.1 ^ 2 + edist x.2 y.2 ^ 2) ^ (1 / 2)
<VAR>α : Type u_1<VAR>inst✝⁴ : Mul α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : One α<VAR>inst✝¹ : OfNat α 2<VAR>inst✝ : Invertible 2<VAR>a b : αˢʸᵐ<GOAL>a * b = b * a
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s✝ s₁ s₂ : Set α✝<VAR>t✝ t₁ t₂ : Set β✝<VAR>a : α✝<VAR>b : β✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>s : Set α<VAR>t : Set β<VAR>p : α × β<GOAL>p ∈ (s ×ˢ t)ᶜ ↔ p ∈ sᶜ ×ˢ univ ∪ univ ×ˢ tᶜ
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s✝ s₁ s₂ : Set α✝<VAR>t✝ t₁ t₂ : Set β✝<VAR>a : α✝<VAR>b : β✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>s : Set α<VAR>t : Set β<VAR>p : α × β<GOAL>p.1 ∈ s → p.2 ∉ t ↔ p.1 ∉ s ∨ p.2 ∉ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hsub : Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<VAR>hn : Set.Icc 0 n = {k | k ≤ n}<GOAL>ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hsub : Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<VAR>hn : Set.Icc 0 n = {k | k ≤ n}<VAR>this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω<GOAL>ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hsub : Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<VAR>hn : Set.Icc 0 n = {k | k ≤ n}<VAR>this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω<VAR>h : ↑ε * (μ {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}).toReal ≤ ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ<GOAL>ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ≤ ENNReal.ofReal (∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hsub : Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<VAR>hn : Set.Icc 0 n = {k | k ≤ n}<VAR>this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω<VAR>h : ↑ε * (μ {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}).toReal ≤ ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ<GOAL>ε • (μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}).toReal ≤ ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hsub : Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<VAR>hn : Set.Icc 0 n = {k | k ≤ n}<VAR>this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω<VAR>h : ↑ε * (μ {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}).toReal ≤ ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ<GOAL>ε • μ {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω} ≠ ⊤
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>𝒢 : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>τ π : Ω → ℕ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hsub : Submartingale f 𝒢 μ<VAR>ε : ℝ≥0<VAR>n : ℕ<VAR>hn : Set.Icc 0 n = {k | k ≤ n}<VAR>this : ∀ (ω : Ω), (↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω) → ↑ε ≤ stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω<VAR>h : ↑ε * (μ {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}).toReal ≤ ∫ (x : Ω) in {a | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k a}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) x ∂μ<GOAL>0 ≤ ∫ (ω : Ω) in {ω | ↑ε ≤ (range (n + 1)).sup' ⋯ fun k => f k ω}, stoppedValue f (hitting f {y | ↑ε ≤ y} 0 n) ω ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x✝ x : α × α<GOAL>x ∈ (s ∩ t).diag ↔ x ∈ s.diag ∩ t.diag
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>S ∈ leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>(∀ (g : G), ∃! s, ↑↑s = ↑g) ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C Y<VAR>U : Opens ↑X<VAR>x : ↥U<VAR>V : Opens ↑Y<VAR>hV : U ≤ (Opens.map f).obj V<GOAL>((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫ ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x = F.germ ⟨f ↑x, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<GOAL>TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformly (fun n => F (u n)) f atTop
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<GOAL>TendstoUniformlyOn F f l univ ↔ ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop univ