ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>(1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>(∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * 1 ^ (k - m) * ↑(k.choose m)) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ 2 ^ m.1 * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ↑(2 ^ m.1) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ↑(∑ m_1 ∈ Finset.range (m.1 + 1), m.1.choose m_1) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (∑ x ∈ Finset.range (m.1 + 1), ↑(m.1.choose x)) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<GOAL>∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<VAR>hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)<GOAL>∑ i ∈ Finset.range (k + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : SMulCommClass ℝ 𝕜 F<VAR>m : ℕ × ℕ<VAR>k n : ℕ<VAR>hk : k ≤ m.1<VAR>hn : n ≤ m.2<VAR>f : 𝓢(E, F)<VAR>x : E<VAR>hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)<GOAL>∑ i ∈ Finset.range (m.1 + 1), ‖x‖ ^ i * ↑(k.choose i) * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ ∑ i ∈ Finset.range (m.1 + 1), ↑(m.1.choose i) * ((Finset.Iic m).sup fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : CommRing C<VAR>p : K[X]<GOAL>integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : CommRing C<VAR>p : K[X]<GOAL>(∀ (n : ℕ), p.coeff n = coeff 0 n) ↔ ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>K : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A K<VAR>inst✝¹ : IsFractionRing A K<VAR>inst✝ : CommRing C<VAR>p : K[X]<VAR>b : A<VAR>nonzero : b ∈ nonZeroDivisors A<VAR>hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i<GOAL>(∀ (n : ℕ), p.coeff n = coeff 0 n) ↔ ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : Cospherical ps<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>hc : ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<GOAL>∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<VAR>sx : Simplex ℝ P n<VAR>hsxps : Set.range sx.points ⊆ ps<GOAL>sx.circumcenter = c
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<VAR>sx : Simplex ℝ P n<VAR>hsxps : Set.range sx.points ⊆ ps<VAR>hsx : affineSpan ℝ (Set.range sx.points) = s<GOAL>sx.circumcenter = c
<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>s : AffineSubspace ℝ P<VAR>ps : Set P<VAR>h : ps ⊆ ↑s<VAR>inst✝¹ : Nonempty ↥s<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ ↥s.direction<VAR>hd : finrank ℝ ↥s.direction = n<VAR>c : P<VAR>hc✝ : c ∈ s<VAR>r : ℝ<VAR>hcr : ∀ p ∈ ps, dist p c = r<VAR>sx : Simplex ℝ P n<VAR>hsxps : Set.range sx.points ⊆ ps<VAR>hsx : affineSpan ℝ (Set.range sx.points) = s<VAR>hc : c ∈ affineSpan ℝ (Set.range sx.points)<GOAL>sx.circumcenter = c
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<GOAL>orderOf 1 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s t✝ : Set α<VAR>ι : Type u_2<VAR>l : ι → Filter α<VAR>t : Set ι<VAR>hd : t.PairwiseDisjoint l<VAR>ht : t.Finite<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s t✝ : Set α<VAR>ι : Type u_2<VAR>l : ι → Filter α<VAR>t : Set ι<VAR>hd : t.PairwiseDisjoint l<VAR>ht : t.Finite<VAR>this : Finite ↑t<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ : Set α<VAR>ι : Type u_2<VAR>l : ι → Filter α<VAR>t : Set ι<VAR>hd : t.PairwiseDisjoint l<VAR>ht : t.Finite<VAR>this : Finite ↑t<VAR>s : ↑t → Set α<VAR>hsl : ∀ (i : ↑t), s i ∈ l ↑i<VAR>hsd : Pairwise (Disjoint on s)<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ : Set α<VAR>ι : Type u_2<VAR>l : ι → Filter α<VAR>t : Set ι<VAR>hd : t.PairwiseDisjoint l<VAR>ht : t.Finite<VAR>this : Finite ↑t<VAR>s : (i : ↑t) → { s // s ∈ l ↑i }<VAR>hsd : Pairwise (Disjoint on fun i => ↑(s i))<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t✝ : Set α<VAR>ι : Type u_2<VAR>l : ι → Filter α<VAR>t : Set ι<VAR>hd : t.PairwiseDisjoint l<VAR>ht : t.Finite<VAR>this : Finite ↑t<VAR>s : (i : ι) → { s // s ∈ l i }<VAR>hsd : Pairwise (Disjoint on fun i => ↑((fun i => s ↑i) i))<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<GOAL>(𝓟 s).IsMeasurablyGenerated ↔ MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<GOAL>(𝓟 s).IsMeasurablyGenerated → MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<VAR>hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<VAR>hs : ∀ ⦃s_1 : Set α⦄, s_1 ∈ 𝓟 s → ∃ t ∈ 𝓟 s, MeasurableSet t ∧ t ⊆ s_1<VAR>t : Set α<VAR>ht : t ∈ 𝓟 s<VAR>htm : MeasurableSet t<VAR>hts : t ⊆ s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>inst✝ : Nonempty β<VAR>x✝ : ∃ f, Injective f<VAR>f : ↑s → β<VAR>hf : Injective f<GOAL>∃ f, InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>inst✝ : Nonempty β<VAR>x✝ : ∃ f, Injective f<VAR>f : α → β<VAR>hf : Injective fun i => f ↑i<GOAL>∃ f, InjOn f s
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>A.adjugate⁻¹ = h.unit⁻¹ • A
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B A : Matrix n n α<VAR>h : IsUnit A.det<GOAL>h.unit⁻¹ • A * A.adjugate = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x : E<VAR>hs : Convex 𝕜 s<VAR>z : E<GOAL>Convex 𝕜 ((fun x => x + z) ⁻¹' s)
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hu : IsUniform X s ℙ μ<GOAL>ProbabilityTheory.cond μ s ≪ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set α<GOAL>(N.comap f).Base B ↔ N.Basis (f '' B) (f '' (f ⁻¹' N.E)) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>B : Set α<GOAL>N.Basis (f '' B) (f '' (N.comap f).E) ∧ InjOn f B ∧ B ⊆ (N.comap f).E ↔ N.Basis (f '' B) (f '' (f ⁻¹' N.E)) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a b : α i<GOAL>update f i '' Ioc a b = Ioc (update f i a) (update f i b)
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.17728<VAR>s✝ t s : Finset α<VAR>i : ℕ<GOAL>Multiset.map val (powersetCard i s).val = Multiset.powersetCard i s.val
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp a b = toIocDiv hp 0 (b - a)
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : ¬BddBelow s<VAR>ha : ¬BddAbove s<GOAL>s = univ
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : ¬BddBelow s<VAR>ha : ¬BddAbove s<VAR>x : α<GOAL>x ∈ s
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : ¬BddBelow s<VAR>ha : ¬BddAbove s<VAR>x y : α<VAR>ys : y ∈ s<VAR>hy : y < x<GOAL>x ∈ s
<VAR>X : Type u<VAR>α : Type v<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>s : Set α<VAR>hs : IsPreconnected s<VAR>hb : ¬BddBelow s<VAR>ha : ¬BddAbove s<VAR>x y : α<VAR>ys : y ∈ s<VAR>hy : y < x<VAR>z : α<VAR>zs : z ∈ s<VAR>hz : x < z<GOAL>x ∈ s
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>v : n → R<GOAL>(∀ i ∈ Finset.univ, star (v i) * v i = 0) ↔ v = 0
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁶ : SeminormedRing 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup M₁<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : NormedSpace 𝕜₁ M₁<VAR>inst✝¹ : Module 𝕜₂ M₂<VAR>inst✝ : ContinuousConstSMul 𝕜₂ M₂<VAR>f : M₁ →ₛₗ[σ₁₂] M₂<VAR>hf : IsCompactOperator ⇑f<VAR>S : Set M₁<VAR>hS : Bornology.IsBounded S<GOAL>IsVonNBounded 𝕜₁ S
<VAR>α : Type u_1<VAR>inst✝³ : Preorder α<VAR>a : α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : NoMaxOrder α<VAR>h : IsSuccLimit a<VAR>b : α<VAR>hb : b ≤ a<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>inst✝³ : Preorder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : NoMaxOrder α<VAR>b : α<VAR>h : IsSuccLimit (succ^[0] b)<VAR>hb : b ≤ succ^[0] b<GOAL>succ^[0] b ≤ b
<VAR>α : Type u_1<VAR>inst✝³ : Preorder α<VAR>inst✝² : SuccOrder α<VAR>inst✝¹ : IsSuccArchimedean α<VAR>inst✝ : NoMaxOrder α<VAR>b : α<VAR>n : ℕ<VAR>h : IsSuccLimit (succ^[n + 1] b)<VAR>hb : b ≤ succ^[n + 1] b<GOAL>succ^[n + 1] b ≤ b
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>x : A<GOAL>IsAlgebraic R x ↔ ¬Function.Injective ⇑(aeval x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h1 : f =ᶠ[𝓝[s] x] g<VAR>h2 : f x = g x<GOAL>P f s x ↔ P g s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h1 : f =ᶠ[𝓝[s] x] g<VAR>h2 : f x = g x<GOAL>P f (s ∩ {x | f x = g x}) x ↔ P g (s ∩ {x | f x = g x}) x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q✝ p q : R[X]<VAR>hpq : p * q ≠ 0<GOAL>(p * q).roots = p.roots + q.roots
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>π : α → Type u_1<VAR>inst✝ : (a : α) → Preorder (π a)<VAR>F : ι → (a : α) → π a<GOAL>BddAbove (range F) ↔ ∀ (a : α), BddAbove (range fun i => F i a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>π : α → Type u_1<VAR>inst✝ : (a : α) → Preorder (π a)<VAR>F : ι → (a : α) → π a<GOAL>(∀ (a : α), BddAbove (range (eval a ∘ F))) ↔ ∀ (a : α), BddAbove (range fun i => F i a)
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<GOAL>LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℕ<VAR>hm : m ≠ 0<GOAL>↑m ≠ 0
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesSummable (fun n => ↑(Λ n)) s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hf : LSeriesSummable (logMul 1) s<GOAL>LSeriesSummable (fun n => ↑(Λ n)) s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hf : Summable fun x => ‖term (logMul 1) s x‖<GOAL>Summable fun x => ‖term (fun n => ↑(Λ n)) s x‖
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hf : Summable fun x => ‖term (logMul 1) s x‖<VAR>n : ℕ<GOAL>‖↑(Λ n)‖ ≤ ‖logMul 1 n‖
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hf : Summable fun x => ‖term (logMul 1) s x‖<VAR>n : ℕ<VAR>hΛ : ‖(fun n => ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖<GOAL>‖↑(Λ n)‖ ≤ ‖logMul 1 n‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>hb : ¬IsMin b<GOAL>pred a ≤ pred b ↔ a ≤ b
<VAR>τ : Type u_1<VAR>inst✝³ : AddMonoid τ<VAR>inst✝² : TopologicalSpace τ<VAR>inst✝¹ : ContinuousAdd τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>f₁ : τ → α → α<VAR>cont'✝¹ : Continuous (uncurry f₁)<VAR>map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)<VAR>map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x<VAR>f₂ : τ → α → α<VAR>cont'✝ : Continuous (uncurry f₂)<VAR>map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)<VAR>map_zero'✝ : ∀ (x : α), f₂ 0 x = x<VAR>h : ∀ (t : τ) (x : α), { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ }.toFun t x = { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }.toFun t x<GOAL>f₁ = f₂
<VAR>τ : Type u_1<VAR>inst✝³ : AddMonoid τ<VAR>inst✝² : TopologicalSpace τ<VAR>inst✝¹ : ContinuousAdd τ<VAR>α : Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>ϕ : Flow τ α<VAR>f₁ : τ → α → α<VAR>cont'✝¹ : Continuous (uncurry f₁)<VAR>map_add'✝¹ : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)<VAR>map_zero'✝¹ : ∀ (x : α), f₁ 0 x = x<VAR>f₂ : τ → α → α<VAR>cont'✝ : Continuous (uncurry f₂)<VAR>map_add'✝ : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)<VAR>map_zero'✝ : ∀ (x : α), f₂ 0 x = x<VAR>h : ∀ (t : τ) (x : α), { toFun := f₁, cont' := cont'✝¹, map_add' := map_add'✝¹, map_zero' := map_zero'✝¹ }.toFun t x = { toFun := f₂, cont' := cont'✝, map_add' := map_add'✝, map_zero' := map_zero'✝ }.toFun t x<VAR>x✝¹ : τ<VAR>x✝ : α<GOAL>f₁ x✝¹ x✝ = f₂ x✝¹ x✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1<GOAL>StrictConvexSpace ℝ E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedLinearOrderedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1<VAR>x : E<VAR>hx : x ∈ closedBall 0 1 \ interior (closedBall 0 1)<VAR>y : E<VAR>hy : y ∈ closedBall 0 1 \ interior (closedBall 0 1)<VAR>hne : x ≠ y<GOAL>(fun x y => ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)) x y