ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(f =O[l] fun x => c • f' x) ↔ f =O[l] f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(f =O[l] fun x => c • f' x) ↔ f =O[l] f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(f =O[l] fun x => ‖c • f' x‖) ↔ f =O[l] f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(f =O[l] fun x => ‖c‖ * ‖f' x‖) ↔ f =O[l] f'
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<GOAL>IsNilpotent R L (M ⧸ N) ↔ ∃ k, lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<GOAL>(∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<GOAL>lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ lowerCentralSeries R L M k ≤ N
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : ContinuousStar A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : Algebra R B<VAR>x : A<GOAL>IsClosed (range Subtype.val)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : TopologicalSemiring A<VAR>inst✝⁶ : ContinuousStar A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : Algebra R B<VAR>x : A<GOAL>range Subtype.val = ↑(elementalStarAlgebra R x)
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n.bit0.size = n.bit0.natSize
<VAR>α : Type u_1<VAR>n : PosNum<GOAL>↑n.bit1.size = n.bit1.natSize
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁷ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁶ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁵ : AddGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>φ : ℕ → α →ₛ E<VAR>hφ : ∀ (x : α), Tendsto (fun n => ↑(φ n) x) atTop (𝓝 (f x))<GOAL>Measurable (f + g)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁷ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁶ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁵ : AddGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>φ : ℕ → α →ₛ E<VAR>hφ : ∀ (x : α), Tendsto (fun n => ↑(φ n) x) atTop (𝓝 (f x))<VAR>this : Tendsto (fun n x => ↑(φ n) x + g x) atTop (𝓝 (f + g))<GOAL>Measurable (f + g)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁷ : Countable ι<VAR>f✝ g✝ : α✝ → β<VAR>mα : MeasurableSpace α✝<VAR>inst✝⁶ : TopologicalSpace β<VAR>α : Type u_5<VAR>E : Type u_6<VAR>x✝ : MeasurableSpace α<VAR>inst✝⁵ : AddGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : PseudoMetrizableSpace E<VAR>g f : α → E<VAR>hg : Measurable g<VAR>φ : ℕ → α →ₛ E<VAR>hφ : ∀ (x : α), Tendsto (fun n => ↑(φ n) x) atTop (𝓝 (f x))<VAR>this : Tendsto (fun n x => ↑(φ n) x + g x) atTop (𝓝 (f + g))<VAR>n : ℕ<GOAL>Measurable fun x => ↑(φ n) x + g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l✝ l' : List α<VAR>a : α<VAR>val✝ : Multiset α<VAR>l : List α<VAR>hl : Multiset.Nodup (Quot.mk Setoid.r l)<VAR>a✝ : { val := Quot.mk Setoid.r l, nodup := hl } ∈ Set.univ<GOAL>{ val := Quot.mk Setoid.r l, nodup := hl } ∈ toFinset '' {l | l.Nodup}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace β<VAR>f✝ f : α → β<VAR>a : α<VAR>s : Set α<VAR>this : TopologicalSpace α := induced f t<GOAL>a ∈ closure s ↔ f a ∈ closure (f '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u_4<VAR>S'' : Type u_5<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>x : P.Ring<GOAL>(g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)
<VAR>A : Type u_1<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : CstarRing A<VAR>inst✝⁴ : CompleteSpace A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : PartialOrder A<VAR>inst✝ : StarOrderedRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>(spectralRadius ℝ a).toReal = ‖a‖
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>inst✝ : Semiring k<VAR>f : k[G]<GOAL>f ∈ Submodule.span k ((fun a => single a 1) '' ↑f.support)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℕ<GOAL>A ^ (↑m * ↑n) = (A ^ ↑m) ^ ↑n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℕ<GOAL>A ^ (↑m * -[n+1]) = (A ^ ↑m) ^ -[n+1]
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℕ<GOAL>A ^ (-[m+1] * ↑n) = (A ^ -[m+1]) ^ ↑n
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℕ<GOAL>A ^ (-[m+1] * -[n+1]) = (A ^ -[m+1]) ^ -[n+1]
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℕ<GOAL>IsUnit (A ^ ((m + 1) * (n + 1))).det
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<VAR>h : IsUnit A.det<VAR>m n : ℕ<GOAL>IsUnit (A.det ^ ((m + 1) * (n + 1)))
<VAR>α : Type u_1<VAR>inst✝¹ : AddMonoidWithOne α<VAR>inst✝ : CharZero α<VAR>n✝¹ n✝ : ℕ<VAR>h : n✝¹.beq n✝ = false<GOAL>¬↑n✝¹ = ↑n✝
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : AddCommGroup N<VAR>f g : M → N<VAR>x y : M<GOAL>polar (f + g) x y = polar f x y + polar g x y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : AddCommGroup N<VAR>f g : M → N<VAR>x y : M<GOAL>f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>hs : s ≠ univ<GOAL>∃ y ∈ frontier s, infDist x sᶜ = dist x y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>hs : s ≠ univ<VAR>y : E<VAR>hys : y ∈ closure sᶜ<VAR>hyd : infDist x sᶜ = dist x y<GOAL>∃ y ∈ frontier s, infDist x sᶜ = dist x y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>hs : s ≠ univ<VAR>y : E<VAR>hys : y ∈ (interior s)ᶜ<VAR>hyd : infDist x sᶜ = dist x y<GOAL>∃ y ∈ frontier s, infDist x sᶜ = dist x y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<VAR>s : Set E<VAR>hx : x ∈ s<VAR>hs : s ≠ univ<VAR>y : E<VAR>hys : y ∈ (interior s)ᶜ<VAR>hyd : infDist x sᶜ = dist x y<GOAL>infDist x sᶜ = dist y x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<GOAL>lift.{v, u} #ι < c.ord.cof
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : CompleteSpace 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Nontrivial E<GOAL>𝔠 ≤ #E
<VAR>𝕜 : Type u<VAR>E : Type v<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : CompleteSpace 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Nontrivial E<VAR>A : lift.{v, u} 𝔠 ≤ lift.{v, u} #𝕜<GOAL>𝔠 ≤ #E
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addX P P = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>K' : Type u_3<VAR>inst✝ : Field K'<VAR>p n : ℕ<VAR>hp : 1 < p<GOAL>(X ^ p - X).natDegree = p
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Fintype K<VAR>K' : Type u_3<VAR>inst✝ : Field K'<VAR>p n : ℕ<VAR>hp : 1 < p<VAR>h1 : X.degree < (X ^ p).degree<GOAL>(X ^ p - X).natDegree = p
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>¬(harmonic n).isInt = true
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>1 < padicNorm 2 (harmonic n)
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>1 < ↑2 ^ Nat.log 2 n
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : Group α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : GroupSeminormClass F α β<VAR>f : F<VAR>x y : α<GOAL>f x ≤ f y + f (y / x)
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>v : ι → α<VAR>l : Line α ι'<VAR>x : α<GOAL>(fun x i => ((vertical v l).idxFun i).getD x) x = Sum.elim v ((fun x i => (l.idxFun i).getD x) x)
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i✝ : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>v : ι → α<VAR>l : Line α ι'<VAR>x : α<VAR>i : ι ⊕ ι'<GOAL>(fun x i => ((vertical v l).idxFun i).getD x) x i = Sum.elim v ((fun x i => (l.idxFun i).getD x) x) i
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsUpperSet ↑ℬ<GOAL>2 ^ Fintype.card α * (𝒜 ∩ ℬ).card ≤ 𝒜.card * ℬ.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsLowerSet ↑𝒜<VAR>hℬ : IsUpperSet ↑ℬ<GOAL>2 ^ Fintype.card α * (ℬ ∩ 𝒜).card ≤ ℬ.card * 𝒜.card
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<GOAL>F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<GOAL>F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)
<VAR>C : Type v₁<VAR>inst✝² : Category.{v₁, v₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : IsFilteredOrEmpty C<GOAL>((∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) ∧ ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t) → ∀ (d : D), IsFiltered (StructuredArrow d F)
<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>inst✝ : CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>Iic (⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, Iic (f i j)
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>(s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑π
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>↑π ^ (-(s / 2)) * (↑π)⁻¹ * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>↑π ^ (-s / 2) * (s * Gamma (s / 2)) * (2 * ↑π) = ↑π ^ (-s / 2) * Gamma (s / 2) * s * (↑π * 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s t : Set α<GOAL>(s \ t).encard + t.encard = (s ∪ t).encard
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<GOAL>(Algebra.norm K) (ζ - 1) = ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<GOAL>(Algebra.norm K) (ζ - 1) = ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<GOAL>(Algebra.norm K) (ζ - 1) = ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<GOAL>(Algebra.norm K) (ζ - 1) = ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<GOAL>(algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝ : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this : FiniteDimensional K L := finiteDimensional {n} K L<GOAL>(algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝¹ : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this✝ : FiniteDimensional K L := finiteDimensional {n} K L<VAR>this : IsGalois K L := isGalois n K L<GOAL>(algebraMap K E) ((Algebra.norm K) (ζ - 1)) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝¹ : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this✝ : FiniteDimensional K L := finiteDimensional {n} K L<VAR>this : IsGalois K L := isGalois n K L<GOAL>∏ σ : L →ₐ[K] E, σ (ζ - 1) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝¹ : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this✝ : FiniteDimensional K L := finiteDimensional {n} K L<VAR>this : IsGalois K L := isGalois n K L<GOAL>∏ x : L →ₐ[K] E, -1 * (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field L<VAR>ζ : L<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>h : 2 < ↑n<VAR>hirr : Irreducible (cyclotomic (↑n) K)<VAR>this✝¹ : NeZero ↑↑n<VAR>E : Type v := AlgebraicClosure L<VAR>z : E<VAR>hz : (cyclotomic (↑n) E).IsRoot z<VAR>this✝ : FiniteDimensional K L := finiteDimensional {n} K L<VAR>this : IsGalois K L := isGalois n K L<GOAL>∏ x : L →ₐ[K] E, (1 - x ζ) = (algebraMap K E) ↑(eval 1 (cyclotomic ↑n ℤ))