ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<VAR>mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure<VAR>frequently_mem_polynomials : ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring<VAR>g : ℝ[X]<GOAL>(g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A.toSubsemiring
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hm : IsPeriodicPt f m (f^[n] x)<VAR>r : ℕ<VAR>hr : r > 0<VAR>hr' : IsPeriodicPt f r x<GOAL>IsPeriodicPt f m x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hm : IsPeriodicPt f m (f^[n] x)<VAR>r : ℕ<VAR>hr : r > 0<VAR>hr' : IsPeriodicPt f r x<GOAL>n ≤ (n / r + 1) * r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hm : IsPeriodicPt f m (f^[n] x)<VAR>r : ℕ<VAR>hr : r > 0<VAR>hr' : IsPeriodicPt f r x<GOAL>n ≤ n / r * r + r
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<GOAL>w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : AEMeasurable f μ<GOAL>0 < μ {x | f x ≤ ∫⁻ (a : α), f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>∫⁻ (a : α), ↑‖f_lim a‖₊ ^ p ∂μ = ∫⁻ (a : α), liminf (fun m => ↑‖f m a‖₊ ^ p) atTop ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>a : α<VAR>ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))<GOAL>(fun a => ↑‖f_lim a‖₊ ^ p) a = (fun a => liminf (fun m => ↑‖f m a‖₊ ^ p) atTop) a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>a : α<VAR>ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))<GOAL>↑‖f_lim a‖₊ ^ p = liminf (fun m => ↑‖f m a‖₊ ^ p) atTop
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>a : α<VAR>ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))<GOAL>Tendsto (fun m => ↑‖f m a‖₊ ^ p) atTop (𝓝 (↑‖f_lim a‖₊ ^ p))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>a : α<VAR>ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))<GOAL>Tendsto (fun a_1 => ‖f a_1 a‖₊ ^ p) atTop (𝓝 (‖f_lim a‖₊ ^ p))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → G<VAR>p : ℝ<VAR>hp_nonneg : 0 ≤ p<VAR>f_lim : α → G<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<VAR>a : α<VAR>ha : Tendsto (fun n => f n a) atTop (𝓝 (f_lim a))<GOAL>Tendsto (fun a_1 => ‖f a_1 a‖₊) atTop (𝓝 ‖f_lim a‖₊)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>g : C(Y, Z)<VAR>y : Y<VAR>hy : f.Homotopic (const X y)<GOAL>(g.comp f).Nullhomotopic
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>g : C(Y, Z)<VAR>y : Y<VAR>hy : f.Homotopic (const X y)<GOAL>(g.comp f).Homotopic (const X (g y))
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S : Set F<VAR>p : F<VAR>hp : p ∈ Ring.closure S<VAR>q : F<VAR>hq : q ∈ Ring.closure S<VAR>r : F<VAR>hr : r ∈ Ring.closure S<VAR>s : F<VAR>hs : s ∈ Ring.closure S<GOAL>p / q * (r / s) ∈ closure S
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>sf 2 * (n + 1) = (∏ i ∈ range (n + 1), (2 * i + 1)!) ^ 2 * 2 ^ (n + 1) * (n + 1)!
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>(2 * n + 1 + 1) * ((2 * n + 1) * (2 * n)!) * ((2 * n + 1) * (2 * n)! * ((∏ x ∈ range n, (2 * x + 1) * (2 * x)!) ^ 2 * 2 ^ n * n !)) = (∏ x ∈ range n, (2 * x + 1) * (2 * x)!) ^ 2 * ((2 * n + 1) ^ 2 * (2 * n)! ^ 2) * 2 ^ (n + 1) * ((n + 1) * n !)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>h : Perfect (closure C)<VAR>x : α<VAR>xC : x ∈ C<GOAL>AccPt x (𝓟 C)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>h : Perfect (closure C)<VAR>x : α<VAR>xC : x ∈ C<VAR>H : AccPt x (𝓟 (closure C))<GOAL>AccPt x (𝓟 C)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>h : Perfect (closure C)<VAR>x : α<VAR>xC : x ∈ C<VAR>H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C<GOAL>∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>h : Perfect (closure C)<VAR>x : α<VAR>xC : x ∈ C<VAR>H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C<VAR>this : ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C<GOAL>∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>h : Perfect (closure C)<VAR>x : α<VAR>xC : x ∈ C<VAR>H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C<VAR>this : ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C<GOAL>∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R✝ M<VAR>N : ι → Submodule R✝ M<VAR>inst✝⁹ : DecidableEq ι<VAR>h : IsInternal N<VAR>R : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>N₁ : ι → Submodule R M₁<VAR>h₁ : IsInternal N₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>N₂ : ι → Submodule R M₂<VAR>h₂ : IsInternal N₂<VAR>κ₁ : ι → Type u_7<VAR>κ₂ : ι → Type u_8<VAR>inst✝³ : (i : ι) → Fintype (κ₁ i)<VAR>inst✝² : ∀ (i : ι), Finite (κ₂ i)<VAR>inst✝¹ : (i : ι) → DecidableEq (κ₁ i)<VAR>inst✝ : Fintype ι<VAR>b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)<VAR>b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)<VAR>f : M₁ →ₗ[R] M₂<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)<VAR>i : ι<VAR>snd✝¹ : κ₂ i<VAR>j : ι<VAR>snd✝ : κ₁ j<GOAL>(toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f ⟨i, snd✝¹⟩ ⟨j, snd✝⟩ = Matrix.blockDiagonal' (fun i => (toMatrix (b₁ i) (b₂ i)) (f.restrict ⋯)) ⟨i, snd✝¹⟩ ⟨j, snd✝⟩
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R✝ M<VAR>N : ι → Submodule R✝ M<VAR>inst✝⁹ : DecidableEq ι<VAR>h : IsInternal N<VAR>R : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>N₁ : ι → Submodule R M₁<VAR>h₁ : IsInternal N₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>N₂ : ι → Submodule R M₂<VAR>h₂ : IsInternal N₂<VAR>κ₁ : ι → Type u_7<VAR>κ₂ : ι → Type u_8<VAR>inst✝³ : (i : ι) → Fintype (κ₁ i)<VAR>inst✝² : ∀ (i : ι), Finite (κ₂ i)<VAR>inst✝¹ : (i : ι) → DecidableEq (κ₁ i)<VAR>inst✝ : Fintype ι<VAR>b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)<VAR>b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)<VAR>f : M₁ →ₗ[R] M₂<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)<VAR>i : ι<VAR>snd✝¹ : κ₂ i<VAR>j : ι<VAR>snd✝ : κ₁ j<GOAL>((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨j, snd✝⟩))) ⟨i, snd✝¹⟩ = if h : i = j then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R✝ M<VAR>N : ι → Submodule R✝ M<VAR>inst✝⁹ : DecidableEq ι<VAR>h : IsInternal N<VAR>R : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>N₁ : ι → Submodule R M₁<VAR>h₁ : IsInternal N₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>N₂ : ι → Submodule R M₂<VAR>h₂ : IsInternal N₂<VAR>κ₁ : ι → Type u_7<VAR>κ₂ : ι → Type u_8<VAR>inst✝³ : (i : ι) → Fintype (κ₁ i)<VAR>inst✝² : ∀ (i : ι), Finite (κ₂ i)<VAR>inst✝¹ : (i : ι) → DecidableEq (κ₁ i)<VAR>inst✝ : Fintype ι<VAR>b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)<VAR>b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)<VAR>f : M₁ →ₗ[R] M₂<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)<VAR>i : ι<VAR>snd✝¹ : κ₂ i<VAR>snd✝ : κ₁ i<GOAL>((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨i, snd✝⟩))) ⟨i, snd✝¹⟩ = if h : i = i then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0
<VAR>ι : Type u_1<VAR>R✝ : Type u_2<VAR>M : Type u_3<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R✝ M<VAR>N : ι → Submodule R✝ M<VAR>inst✝⁹ : DecidableEq ι<VAR>h : IsInternal N<VAR>R : Type u_4<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M₁<VAR>N₁ : ι → Submodule R M₁<VAR>h₁ : IsInternal N₁<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>N₂ : ι → Submodule R M₂<VAR>h₂ : IsInternal N₂<VAR>κ₁ : ι → Type u_7<VAR>κ₂ : ι → Type u_8<VAR>inst✝³ : (i : ι) → Fintype (κ₁ i)<VAR>inst✝² : ∀ (i : ι), Finite (κ₂ i)<VAR>inst✝¹ : (i : ι) → DecidableEq (κ₁ i)<VAR>inst✝ : Fintype ι<VAR>b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)<VAR>b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)<VAR>f : M₁ →ₗ[R] M₂<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)<VAR>i : ι<VAR>snd✝¹ : κ₂ i<VAR>j : ι<VAR>snd✝ : κ₁ j<VAR>hij : i ≠ j<GOAL>((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨j, snd✝⟩))) ⟨i, snd✝¹⟩ = if h : i = j then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>x : E<VAR>r : ℝ<VAR>x✝ : E<GOAL>x✝ ∈ (p.comp f).closedBall x r ↔ x✝ ∈ ⇑f ⁻¹' p.closedBall (f x) r
<VAR>f : ℕ → ℂ<VAR>h : f 1 = 1<GOAL>f * δ = δ
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<GOAL>Continuous fun μ => μ.mass
<VAR>Ω : Type u_1<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁵ : SMul R ℝ≥0<VAR>inst✝⁴ : SMul R ℝ≥0∞<VAR>inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<GOAL>Continuous fun μ => μ.testAgainstNN 1
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>fourierCoeff (liftIco T a f) n = fourierCoeffOn ⋯ f n
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>(1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x = (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • liftIco T a f ↑x ∂volume = ∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • f x ∂volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<GOAL>∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • liftIco T a f ↑t ∂volume = ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • f t ∂volume
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>E : Type<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>a : ℝ<VAR>f : ℝ → ℂ<VAR>n : ℤ<VAR>x : ℝ<VAR>hx : x ∈ Ioo a (a + T)<GOAL>(fourier (-n)) ↑x • liftIco T a f ↑x = (fourier (-n)) ↑x • f x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>hv : v ∈ s.direction<VAR>p : P<VAR>hp : p ∈ s<GOAL>v +ᵥ p ∈ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>hv : ∃ p1 ∈ s, ∃ p2 ∈ s, v = p1 -ᵥ p2<VAR>p : P<VAR>hp : p ∈ s<GOAL>v +ᵥ p ∈ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>p : P<VAR>hp : p ∈ s<VAR>p1 : P<VAR>hp1 : p1 ∈ s<VAR>p2 : P<VAR>hp2 : p2 ∈ s<VAR>hv : v = p1 -ᵥ p2<GOAL>p1 -ᵥ p2 +ᵥ p ∈ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>p : P<VAR>hp : p ∈ s<VAR>p1 : P<VAR>hp1 : p1 ∈ s<VAR>p2 : P<VAR>hp2 : p2 ∈ s<VAR>hv : v = p1 -ᵥ p2<GOAL>p1 -ᵥ p2 +ᵥ p ∈ s ↔ 1 • (p1 -ᵥ p2) +ᵥ p ∈ s.carrier
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>v : V<VAR>p : P<VAR>hp : p ∈ s<VAR>p1 : P<VAR>hp1 : p1 ∈ s<VAR>p2 : P<VAR>hp2 : p2 ∈ s<VAR>hv : v = p1 -ᵥ p2<GOAL>p1 -ᵥ p2 +ᵥ p ∈ s ↔ p1 -ᵥ p2 +ᵥ p ∈ s.carrier
<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>n : ℕ<VAR>s : 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>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 2)<VAR>i₁ i₂ : Fin (n + 3)<GOAL>mk' (centroid ℝ {i₁, i₂}ᶜ s.points) (Submodule.span ℝ {s.points i₁ -ᵥ s.points i₂})ᗮ ⊓ affineSpan ℝ (Set.range s.points) = mk' (centroid ℝ {i₂, i₁}ᶜ s.points) (Submodule.span ℝ {s.points i₂ -ᵥ s.points i₁})ᗮ ⊓ affineSpan ℝ (Set.range s.points)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₀ n₁ n₂ : ℤ<VAR>z : Cochain F G n₀<VAR>h₁₂ : n₁ + 1 = n₂<VAR>h₀₁ : n₀ + 1 = n₁<VAR>p q : ℤ<VAR>hpq : p + n₂ = q<GOAL>(δ n₁ n₂ (δ n₀ n₁ z)).v p q hpq = 0
<VAR>α✝ : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α✝<VAR>s : Set α✝<VAR>α : Type u_2<VAR>U : Set α<VAR>h : IsOpen U<GOAL>U = ∅ ∨ U = univ
<VAR>α✝ : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α✝<VAR>s : Set α✝<VAR>α : Type u_2<GOAL>IsOpen ∅
<VAR>α✝ : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α✝<VAR>s : Set α✝<VAR>α : Type u_2<GOAL>IsOpen univ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hf : Integrable f μ<GOAL>μ[f|m] =ᶠ[ae μ] ↑↑((condexpL1CLM F' hm μ) (Integrable.toL1 f hf))
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hf : Integrable f μ<VAR>x : α<GOAL>↑↑(condexpL1 hm μ f) x = ↑↑((condexpL1CLM F' hm μ) (Integrable.toL1 f hf)) x
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>f✝ f g : R[X]<VAR>I : Ideal R<GOAL>(quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (of f) I)) ((mk f) g)) = (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<GOAL>‖Real.log (abs z)‖ ≤ 1 * ‖Real.log √2 + Real.log (max z.re |z.im|)‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<GOAL>‖Real.log (abs z)‖ ≤ 1 * ‖Real.log √2 + Real.log (max z.re |z.im|)‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>‖Real.log (abs z)‖ ≤ 1 * ‖Real.log √2 + Real.log (max z.re |z.im|)‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>Real.log (abs z) ≤ ‖Real.log √2 + Real.log (max z.re |z.im|)‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>Real.log (abs z) ≤ Real.log √2 + Real.log (max z.re |z.im|)
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>abs z ≤ √2 * max |z.re| |z.im|
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>0 < abs z
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>0 < √2 * max z.re |z.im|
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>√2 ≠ 0
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>z : ℂ<VAR>hz : 1 ≤ z.re<VAR>h2 : 0 < √2<VAR>hz' : 1 ≤ abs z<VAR>hm₀ : 0 < max z.re |z.im|<GOAL>max z.re |z.im| ≠ 0
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<GOAL>∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<VAR>z : ℂ<VAR>hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖<VAR>him : |z.im| ^ n ≤ Real.exp z.re<VAR>h₁ : 1 < z.re<GOAL>↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<VAR>z : ℂ<VAR>hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖<VAR>him : |z.im| ^ n ≤ Real.exp z.re<VAR>h₁ : 1 < z.re<VAR>hle : |z.im| ≤ z.re<GOAL>↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>n : ℕ<VAR>z : ℂ<VAR>hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖<VAR>him : |z.im| ^ n ≤ Real.exp z.re<VAR>h₁ : 1 < z.re<VAR>hle : z.re ≤ |z.im|<GOAL>↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>hp : MeasurableSet {x | p x}<VAR>h : ∀ᵐ (b : β) ∂κ a, ∀ᵐ (c : γ) ∂η (a, b), p (b, c)<GOAL>∀ᵐ (bc : β × γ) ∂(κ ⊗ₖ η) a, p bc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>hp : MeasurableSet {x | p x}<VAR>h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0<GOAL>((κ ⊗ₖ η) a) {a | ¬p a} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>hp : MeasurableSet {x | p x}<VAR>h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0<GOAL>(fun b => (η (a, b)) (Prod.mk b ⁻¹' {a | ¬p a})) =ᶠ[ae (κ a)] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>p : β × γ → Prop<VAR>hp : MeasurableSet {x | p x}<VAR>h : (κ a) {a_1 | ¬(η (a, a_1)) {a | ¬p (a_1, a)} = 0} = 0<GOAL>MeasurableSet {a | ¬p a}
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x : (i : ι) → β i<GOAL>hammingDist x x = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x : (i : ι) → β i<GOAL>∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1