From 302fcdddb00022356472ec756eb15fd94a4151b3 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 19 Feb 2024 15:33:36 +0100 Subject: [PATCH 1/3] Replace Lean3 syntax "lamba x, _" by Lean4 syntax "fun x \maps _" in doc comments. This is close to exhaustive. --- Mathlib/Analysis/BoxIntegral/Basic.lean | 4 ++-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 2 +- Mathlib/Analysis/Calculus/FDeriv/Mul.lean | 2 +- .../Analysis/Calculus/ParametricIntegral.lean | 6 ++--- Mathlib/Analysis/Complex/OpenMapping.lean | 4 ++-- .../Analysis/Fourier/PoissonSummation.lean | 2 +- .../Fourier/RiemannLebesgueLemma.lean | 6 ++--- Mathlib/Analysis/InnerProductSpace/Basic.lean | 3 ++- .../InnerProductSpace/LinearPMap.lean | 4 ++-- .../Analysis/InnerProductSpace/Rayleigh.lean | 8 +++---- .../NormedSpace/Star/Exponential.lean | 4 ++-- .../Analysis/NormedSpace/Star/Multiplier.lean | 4 ++-- .../SpecialFunctions/ImproperIntegrals.lean | 2 +- .../CategoryTheory/Adjunction/Reflective.lean | 4 ++-- .../Limits/Shapes/WideEqualizers.lean | 4 ++-- Mathlib/Data/Matrix/Basic.lean | 2 +- Mathlib/Data/Ordmap/Ordnode.lean | 2 +- Mathlib/Geometry/Manifold/Diffeomorph.lean | 2 +- .../Geometry/Manifold/PartitionOfUnity.lean | 12 +++++----- .../Matrix/GeneralLinearGroup.lean | 5 ++-- Mathlib/Logic/Embedding/Basic.lean | 3 ++- Mathlib/MeasureTheory/Function/L2Space.lean | 4 ++-- .../Integral/CircleIntegral.lean | 4 ++-- .../Integral/DivergenceTheorem.lean | 7 +++--- .../Measure/Lebesgue/Integral.lean | 2 +- Mathlib/ModelTheory/DirectLimit.lean | 4 ++-- Mathlib/Order/Filter/AtTopBot.lean | 24 +++++++++---------- .../Probability/Distributions/Poisson.lean | 2 +- Mathlib/RingTheory/WittVector/IsPoly.lean | 2 +- Mathlib/Tactic/SimpRw.lean | 2 +- .../Topology/Algebra/InfiniteSum/Ring.lean | 2 +- Mathlib/Topology/Algebra/Polynomial.lean | 2 +- .../Topology/Algebra/UniformMulAction.lean | 2 +- Mathlib/Topology/Homotopy/HSpaces.lean | 4 ++-- test/Simps.lean | 4 ++-- 35 files changed, 77 insertions(+), 73 deletions(-) diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean index a891a13fd6b74..0b42b7b169452 100644 --- a/Mathlib/Analysis/BoxIntegral/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Basic.lean @@ -638,7 +638,7 @@ theorem tendsto_integralSum_sum_integral (h : Integrable I l f vol) (π₀ : Pre exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU #align box_integral.integrable.tendsto_integral_sum_sum_integral BoxIntegral.Integrable.tendsto_integralSum_sum_integral -/-- If `f` is integrable on `I`, then `λ J, integral J l f vol` is box-additive on subboxes of `I`: +/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of `I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, then the sum of integrals of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`. @@ -651,7 +651,7 @@ theorem sum_integral_congr (h : Integrable I l f vol) {π₁ π₂ : Prepartitio exact h.tendsto_integralSum_sum_integral π₂ #align box_integral.integrable.sum_integral_congr BoxIntegral.Integrable.sum_integral_congr -/-- If `f` is integrable on `I`, then `λ J, integral J l f vol` is box-additive on subboxes of `I`: +/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of `I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, then the sum of integrals of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`. diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index ec7d1b5810933..5b0eb3e9cf3e0 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -562,7 +562,7 @@ in any universe in `u, v, w, max u v, max v w, max u v w`, but it would be extre lead to a lot of duplication. Instead, we formulate the above proof when all spaces live in the same universe (where everything is fine), and then we deduce the general result by lifting all our spaces to a common universe. We use the trick that any space `H` is isomorphic through a continuous linear -equiv to `ContinuousMultilinearMap (λ (i : Fin 0), E × F × G) H` to change the universe level, +equiv to `ContinuousMultilinearMap (fun (i : Fin 0) ↦ E × F × G) H` to change the universe level, and then argue that composing with such a linear equiv does not change the fact of being `C^n`, which we have already proved previously. -/ diff --git a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean index c803e2e451c0a..ed48bef00e69a 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Mul.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Mul.lean @@ -639,7 +639,7 @@ variable {R : Type*} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpac open NormedRing ContinuousLinearMap Ring /-- At an invertible element `x` of a normed division algebra `R`, the Fréchet derivative of the -inversion operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`. -/ +inversion operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`. -/ theorem hasFDerivAt_inv' {x : R} (hx : x ≠ 0) : HasFDerivAt Inv.inv (-mulLeftRight 𝕜 R x⁻¹ x⁻¹) x := by simpa using hasFDerivAt_ring_inverse (Units.mk0 _ hx) #align has_fderiv_at_inv' hasFDerivAt_inv' diff --git a/Mathlib/Analysis/Calculus/ParametricIntegral.lean b/Mathlib/Analysis/Calculus/ParametricIntegral.lean index 4770293467162..74d7c5548be82 100644 --- a/Mathlib/Analysis/Calculus/ParametricIntegral.lean +++ b/Mathlib/Analysis/Calculus/ParametricIntegral.lean @@ -11,7 +11,7 @@ import Mathlib.MeasureTheory.Integral.SetIntegral /-! # Derivatives of integrals depending on parameters -A parametric integral is a function with shape `f = λ x : H, ∫ a : α, F x a ∂μ` for some +A parametric integral is a function with shape `f = fun x : H ↦ ∫ a : α, F x a ∂μ` for some `F : H → α → E`, where `H` and `E` are normed spaces and `α` is a measured space with measure `μ`. We already know from `continuous_of_dominated` in `Mathlib/MeasureTheory/Integral/Bochner.lean` how @@ -31,8 +31,8 @@ variable. - `F x` is ae-measurable for x near `x₀`, - `F x₀` is integrable, - `fun x ↦ F x a` has derivative `F' a : H →L[ℝ] E` at `x₀` which is ae-measurable, - - `λ x, F x a` is locally Lipschitz near `x₀` for almost every `a`, with a Lipschitz bound which - is integrable with respect to `a`. + - `fun x ↦ F x a` is locally Lipschitz near `x₀` for almost every `a`, + with a Lipschitz bound which is integrable with respect to `a`. A subtle point is that the "near x₀" in the last condition has to be uniform in `a`. This is controlled by a positive number `ε`. diff --git a/Mathlib/Analysis/Complex/OpenMapping.lean b/Mathlib/Analysis/Complex/OpenMapping.lean index 8155fc0ee80f7..11f005bdc8bd0 100644 --- a/Mathlib/Analysis/Complex/OpenMapping.lean +++ b/Mathlib/Analysis/Complex/OpenMapping.lean @@ -21,7 +21,7 @@ its image `f z₀`. The results extend in higher dimension to `g : E → ℂ`. The proof of the local version on `ℂ` goes through two main steps: first, assuming that the function is not constant around `z₀`, use the isolated zero principle to show that `‖f z‖` is bounded below on a small `sphere z₀ r` around `z₀`, and then use the maximum principle applied to the auxiliary -function `(λ z, ‖f z - v‖)` to show that any `v` close enough to `f z₀` is in `f '' ball z₀ r`. That +function `(fun z ↦ ‖f z - v‖)` to show that any `v` close enough to `f z₀` is in `f '' ball z₀ r`. That second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`. ## Main results @@ -45,7 +45,7 @@ theorem DiffContOnCl.ball_subset_image_closedBall (h : DiffContOnCl ℂ f (ball (hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖) (hz₀ : ∃ᶠ z in 𝓝 z₀, f z ≠ f z₀) : ball (f z₀) (ε / 2) ⊆ f '' closedBall z₀ r := by /- This is a direct application of the maximum principle. Pick `v` close to `f z₀`, and look at - the function `λ z, ‖f z - v‖`: it is bounded below on the circle, and takes a small value + the function `fun z ↦ ‖f z - v‖`: it is bounded below on the circle, and takes a small value at `z₀` so it is not constant on the disk, which implies that its infimum is equal to `0` and hence that `v` is in the range of `f`. -/ rintro v hv diff --git a/Mathlib/Analysis/Fourier/PoissonSummation.lean b/Mathlib/Analysis/Fourier/PoissonSummation.lean index db4167ded9a5e..18545b9ea181d 100644 --- a/Mathlib/Analysis/Fourier/PoissonSummation.lean +++ b/Mathlib/Analysis/Fourier/PoissonSummation.lean @@ -129,7 +129,7 @@ section RpowDecay variable {E : Type*} [NormedAddCommGroup E] /-- If `f` is `O(x ^ (-b))` at infinity, then so is the function -`λ x, ‖f.restrict (Icc (x + R) (x + S))‖` for any fixed `R` and `S`. -/ +`fun x ↦ ‖f.restrict (Icc (x + R) (x + S))‖` for any fixed `R` and `S`. -/ theorem isBigO_norm_Icc_restrict_atTop {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b) (hf : f =O[atTop] fun x : ℝ => |x| ^ (-b)) (R S : ℝ) : (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atTop] fun x : ℝ => |x| ^ (-b) := by diff --git a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean index 2b7e71dc5a8c5..611dd80dc8f35 100644 --- a/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean +++ b/Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean @@ -35,11 +35,11 @@ equivalence to an inner-product space. ## Main results - `tendsto_integral_exp_inner_smul_cocompact` : for `V` a finite-dimensional real inner product - space and `f : V → E`, the function `λ w : V, ∫ v : V, exp (2 * π * ⟪w, v⟫ * I) • f v` tends to 0 - along `cocompact V`. + space and `f : V → E`, the function `fun w : V ↦ ∫ v : V, exp (2 * π * ⟪w, v⟫ * I) • f v` + tends to 0 along `cocompact V`. - `tendsto_integral_exp_smul_cocompact` : for `V` a finite-dimensional real vector space (endowed with its unique Hausdorff topological vector space structure), and `W` the dual of `V`, the - function `λ w : W, ∫ v : V, exp (2 * π * w v * I) • f v` tends to along `cocompact W`. + function `fun w : W ↦ ∫ v : V, exp (2 * π * w v * I) • f v` tends to along `cocompact W`. - `Real.tendsto_integral_exp_smul_cocompact`: special case of functions on `ℝ`. - `Real.zero_at_infty_fourierIntegral` and `Real.zero_at_infty_vector_fourierIntegral`: reformulations explicitly using the Fourier integral. diff --git a/Mathlib/Analysis/InnerProductSpace/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Basic.lean index 74f3c3403ec25..93d661901a43f 100644 --- a/Mathlib/Analysis/InnerProductSpace/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Basic.lean @@ -2270,7 +2270,8 @@ end Continuous section ReApplyInnerSelf -/-- Extract a real bilinear form from an operator `T`, by taking the pairing `λ x, re ⟪T x, x⟫`. -/ +/-- Extract a real bilinear form from an operator `T`, +by taking the pairing `fun x ↦ re ⟪T x, x⟫`. -/ def ContinuousLinearMap.reApplyInnerSelf (T : E →L[𝕜] E) (x : E) : ℝ := re ⟪T x, x⟫ #align continuous_linear_map.re_apply_inner_self ContinuousLinearMap.reApplyInnerSelf diff --git a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean index 0a29af06cc725..ae3f8a2925a14 100644 --- a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean +++ b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean @@ -95,8 +95,8 @@ def adjointDomain : Submodule 𝕜 F where exact hx.const_smul (conj a) #align linear_pmap.adjoint_domain LinearPMap.adjointDomain -/-- The operator `λ x, ⟪y, T x⟫` considered as a continuous linear operator from `T.adjointDomain` -to `𝕜`. -/ +/-- The operator `fun x ↦ ⟪y, T x⟫` considered as a continuous linear operator +from `T.adjointDomain` to `𝕜`. -/ def adjointDomainMkCLM (y : T.adjointDomain) : T.domain →L[𝕜] 𝕜 := ⟨(innerₛₗ 𝕜 (y : F)).comp T.toFun, y.prop⟩ #align linear_pmap.adjoint_domain_mk_clm LinearPMap.adjointDomainMkCLM diff --git a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean index 90cb6a1461bbd..d811cbd686d5a 100644 --- a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean +++ b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean @@ -15,18 +15,18 @@ import Mathlib.LinearAlgebra.Eigenspace.Basic # The Rayleigh quotient The Rayleigh quotient of a self-adjoint operator `T` on an inner product space `E` is the function -`λ x, ⟪T x, x⟫ / ‖x‖ ^ 2`. +`fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2`. The main results of this file are `IsSelfAdjoint.hasEigenvector_of_isMaxOn` and `IsSelfAdjoint.hasEigenvector_of_isMinOn`, which state that if `E` is complete, and if the Rayleigh quotient attains its global maximum/minimum over some sphere at the point `x₀`, then `x₀` -is an eigenvector of `T`, and the `iSup`/`iInf` of `λ x, ⟪T x, x⟫ / ‖x‖ ^ 2` is the corresponding +is an eigenvector of `T`, and the `iSup`/`iInf` of `fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2` is the corresponding eigenvalue. The corollaries `LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional` and `LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional` state that if `E` is finite-dimensional and nontrivial, then `T` has some (nonzero) eigenvectors with eigenvalue the -`iSup`/`iInf` of `λ x, ⟪T x, x⟫ / ‖x‖ ^ 2`. +`iSup`/`iInf` of `fun x ↦ ⟪T x, x⟫ / ‖x‖ ^ 2`. ## TODO @@ -125,7 +125,7 @@ theorem linearly_dependent_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : F} ext x simp [dist_eq_norm] -- find Lagrange multipliers for the function `T.re_apply_inner_self` and the - -- hypersurface-defining function `λ x, ‖x‖ ^ 2` + -- hypersurface-defining function `fun x ↦ ‖x‖ ^ 2` obtain ⟨a, b, h₁, h₂⟩ := IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d H (hasStrictFDerivAt_norm_sq x₀) (hT.isSymmetric.hasStrictFDerivAt_reApplyInnerSelf x₀) diff --git a/Mathlib/Analysis/NormedSpace/Star/Exponential.lean b/Mathlib/Analysis/NormedSpace/Star/Exponential.lean index 7b34ba93e4206..008811ac5ceda 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Exponential.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Exponential.lean @@ -8,8 +8,8 @@ import Mathlib.Analysis.NormedSpace.Exponential #align_import analysis.normed_space.star.exponential from "leanprover-community/mathlib"@"1e3201306d4d9eb1fd54c60d7c4510ad5126f6f9" /-! # The exponential map from selfadjoint to unitary -In this file, we establish various properties related to the map `λ a, exp ℂ A (I • a)` between the -subtypes `selfAdjoint A` and `unitary A`. +In this file, we establish various properties related to the map `fun a ↦ exp ℂ A (I • a)` +between the subtypes `selfAdjoint A` and `unitary A`. ## TODO diff --git a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean index f7c3864bf567d..38b458ac569cc 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Multiplier.lean @@ -99,8 +99,8 @@ variable [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] Because the multiplier algebra is defined as the algebra of double centralizers, there is a natural injection `DoubleCentralizer.toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ` -defined by `λ a, (a.fst, MulOpposite.op a.snd)`. We use this map to pull back the ring, module and -algebra structure from `(A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ` to `𝓜(𝕜, A)`. -/ +defined by `fun a ↦ (a.fst, MulOpposite.op a.snd)`. We use this map to pull back the ring, module +and algebra structure from `(A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ` to `𝓜(𝕜, A)`. -/ variable {𝕜 A} diff --git a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean index fa45a9c7b8b74..8c2a69c2c7ac3 100644 --- a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean @@ -58,7 +58,7 @@ theorem integral_exp_neg_Ioi_zero : (∫ x : ℝ in Ioi 0, exp (-x)) = 1 := by simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0 #align integral_exp_neg_Ioi_zero integral_exp_neg_Ioi_zero -/-- If `0 < c`, then `(λ t : ℝ, t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/ +/-- If `0 < c`, then `(fun t : ℝ ↦ t ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/ theorem integrableOn_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) : IntegrableOn (fun t : ℝ => t ^ a) (Ioi c) := by have hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x := by diff --git a/Mathlib/CategoryTheory/Adjunction/Reflective.lean b/Mathlib/CategoryTheory/Adjunction/Reflective.lean index a58284272d894..c657807790f15 100644 --- a/Mathlib/CategoryTheory/Adjunction/Reflective.lean +++ b/Mathlib/CategoryTheory/Adjunction/Reflective.lean @@ -122,8 +122,8 @@ theorem unitCompPartialBijectiveAux_symm_apply [Reflective i] {A : C} {B : D} /-- If `i` has a reflector `L`, then the function `(i.obj (L.obj A) ⟶ B) → (A ⟶ B)` given by precomposing with `η.app A` is a bijection provided `B` is in the essential image of `i`. -That is, the function `λ (f : i.obj (L.obj A) ⟶ B), η.app A ≫ f` is bijective, as long as `B` is in -the essential image of `i`. +That is, the function `fun (f : i.obj (L.obj A) ⟶ B) ↦ η.app A ≫ f` is bijective, +as long as `B` is in the essential image of `i`. This definition gives an equivalence: the key property that the inverse can be described nicely is shown in `unitCompPartialBijective_symm_apply`. diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean index 739046ae22b96..367c12fa7e838 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean @@ -429,8 +429,8 @@ theorem Cotrident.IsColimit.homIso_natural [Nonempty J] {t : Cotrident f} {Z Z' /-- This is a helper construction that can be useful when verifying that a category has certain wide equalizers. Given `F : WalkingParallelFamily ⥤ C`, which is really the same as - `parallelFamily (λ j, F.map (line j))`, and a trident on `λ j, F.map (line j)`, we get a cone - on `F`. + `parallelFamily (λ j, F.map (line j))`, and a trident on `fun j ↦ F.map (line j)`, + we get a cone on `F`. If you're thinking about using this, have a look at `hasWideEqualizers_of_hasLimit_parallelFamily`, which you may find to be an easier way of diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean index 2760228204bed..1463d784f21c2 100644 --- a/Mathlib/Data/Matrix/Basic.lean +++ b/Mathlib/Data/Matrix/Basic.lean @@ -41,7 +41,7 @@ The locale `Matrix` gives the following notation: For convenience, `Matrix m n α` is defined as `m → n → α`, as this allows elements of the matrix to be accessed with `A i j`. However, it is not advisable to _construct_ matrices using terms of the -form `λ i j, _` or even `(λ i j, _ : Matrix m n α)`, as these are not recognized by lean as having +form `fun i j ↦ _` or even `(fun i j ↦ _ : Matrix m n α)`, as these are not recognized by lean as having the right type. Instead, `Matrix.of` should be used. ## TODO diff --git a/Mathlib/Data/Ordmap/Ordnode.lean b/Mathlib/Data/Ordmap/Ordnode.lean index 8f1477784ccb2..699511092c826 100644 --- a/Mathlib/Data/Ordmap/Ordnode.lean +++ b/Mathlib/Data/Ordmap/Ordnode.lean @@ -596,7 +596,7 @@ Case conversion may be inaccurate. Consider using '#align ordnode.map Ordnode.ma the function is strictly monotone, i.e. `x < y → f x < f y`. partition (fun x ↦ x + 2) {1, 2, 4} = {2, 3, 6} - partition (λ x : ℕ, x - 2) {1, 2, 4} = precondition violation -/ + partition (fun x : ℕ ↦ x - 2) {1, 2, 4} = precondition violation -/ def map {β} (f : α → β) : Ordnode α → Ordnode β | nil => nil | node s l x r => node s (map f l) (f x) (map f r) diff --git a/Mathlib/Geometry/Manifold/Diffeomorph.lean b/Mathlib/Geometry/Manifold/Diffeomorph.lean index 920c81a8fb57b..b4fe6e8ccebf5 100644 --- a/Mathlib/Geometry/Manifold/Diffeomorph.lean +++ b/Mathlib/Geometry/Manifold/Diffeomorph.lean @@ -161,7 +161,7 @@ theorem toEquiv_inj {h h' : M ≃ₘ^n⟮I, I'⟯ M'} : h.toEquiv = h'.toEquiv toEquiv_injective.eq_iff #align diffeomorph.to_equiv_inj Diffeomorph.toEquiv_inj -/-- Coercion to function `λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M')` is injective. -/ +/-- Coercion to function `fun h : M ≃ₘ^n⟮I, I'⟯ M' ↦ (h : M → M')` is injective. -/ theorem coeFn_injective : Injective ((↑) : (M ≃ₘ^n⟮I, I'⟯ M') → (M → M')) := DFunLike.coe_injective #align diffeomorph.coe_fn_injective Diffeomorph.coeFn_injective diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index c3080511cd16d..9415a89590a8d 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -89,7 +89,7 @@ variable (ι M) /-- We say that a collection of `SmoothBumpFunction`s is a `SmoothBumpCovering` of a set `s` if * `(f i).c ∈ s` for all `i`; -* the family `λ i, support (f i)` is locally finite; +* the family `fun i ↦ support (f i)` is locally finite; * for each point `x ∈ s` there exists `i` such that `f i =ᶠ[𝓝 x] 1`; in other words, `x` belongs to the interior of `{y | f i y = 1}`; @@ -116,7 +116,7 @@ structure SmoothBumpCovering (s : Set M := univ) where /-- We say that a collection of functions form a smooth partition of unity on a set `s` if * all functions are infinitely smooth and nonnegative; -* the family `λ i, support (f i)` is locally finite; +* the family `fun i ↦ support (f i)` is locally finite; * for all `x ∈ s` the sum `∑ᶠ i, f i x` equals one; * for all `x`, the sum `∑ᶠ i, f i x` is less than or equal to one. -/ structure SmoothPartitionOfUnity (s : Set M := univ) where @@ -196,7 +196,7 @@ theorem smooth_smul {g : M → F} {i} (hg : ∀ x ∈ tsupport (f i), SmoothAt I /-- If `f` is a smooth partition of unity on a set `s : Set M` and `g : ι → M → F` is a family of functions such that `g i` is $C^n$ smooth at every point of the topological support of `f i`, then -the sum `λ x, ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/ +the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/ theorem contMDiff_finsum_smul {g : ι → M → F} (hg : ∀ (i), ∀ x ∈ tsupport (f i), ContMDiffAt I 𝓘(ℝ, F) n (g i) x) : ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ i, f i x • g i x := @@ -206,7 +206,7 @@ theorem contMDiff_finsum_smul {g : ι → M → F} /-- If `f` is a smooth partition of unity on a set `s : Set M` and `g : ι → M → F` is a family of functions such that `g i` is smooth at every point of the topological support of `f i`, then the sum -`λ x, ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/ +`fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/ theorem smooth_finsum_smul {g : ι → M → F} (hg : ∀ (i), ∀ x ∈ tsupport (f i), SmoothAt I 𝓘(ℝ, F) (g i) x) : Smooth I 𝓘(ℝ, F) fun x => ∑ᶠ i, f i x • g i x := @@ -310,7 +310,7 @@ alias ⟨_, IsSubordinate.toPartitionOfUnity⟩ := isSubordinate_toPartitionOfUn /-- If `f` is a smooth partition of unity on a set `s : Set M` subordinate to a family of open sets `U : ι → Set M` and `g : ι → M → F` is a family of functions such that `g i` is $C^n$ smooth on -`U i`, then the sum `λ x, ∑ᶠ i, f i x • g i x` is $C^n$ smooth on the whole manifold. -/ +`U i`, then the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is $C^n$ smooth on the whole manifold. -/ theorem IsSubordinate.contMDiff_finsum_smul {g : ι → M → F} (hf : f.IsSubordinate U) (ho : ∀ i, IsOpen (U i)) (hg : ∀ i, ContMDiffOn I 𝓘(ℝ, F) n (g i) (U i)) : ContMDiff I 𝓘(ℝ, F) n fun x => ∑ᶠ i, f i x • g i x := @@ -319,7 +319,7 @@ theorem IsSubordinate.contMDiff_finsum_smul {g : ι → M → F} (hf : f.IsSubor /-- If `f` is a smooth partition of unity on a set `s : Set M` subordinate to a family of open sets `U : ι → Set M` and `g : ι → M → F` is a family of functions such that `g i` is smooth on `U i`, -then the sum `λ x, ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/ +then the sum `fun x ↦ ∑ᶠ i, f i x • g i x` is smooth on the whole manifold. -/ theorem IsSubordinate.smooth_finsum_smul {g : ι → M → F} (hf : f.IsSubordinate U) (ho : ∀ i, IsOpen (U i)) (hg : ∀ i, SmoothOn I 𝓘(ℝ, F) (g i) (U i)) : Smooth I 𝓘(ℝ, F) fun x => ∑ᶠ i, f i x • g i x := diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean index 5b0bb737fd2e4..47c851b8ff0aa 100644 --- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean +++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean @@ -128,10 +128,11 @@ def toLinear : GeneralLinearGroup n R ≃* LinearMap.GeneralLinearGroup R (n → Units.mapEquiv Matrix.toLinAlgEquiv'.toRingEquiv.toMulEquiv #align matrix.general_linear_group.to_linear Matrix.GeneralLinearGroup.toLinear --- Note that without the `@` and `‹_›`, lean infers `λ a b, _inst a b` instead of `_inst` as the +-- Note that without the `@` and `‹_›`, lean infers `fun a b ↦ _inst a b` instead of `_inst` as the -- decidability argument, which prevents `simp` from obtaining the instance by unification. --- These `λ a b, _inst a b` terms also appear in the type of `A`, but simp doesn't get confused by +-- These `fun a b ↦ _inst a b` terms also appear in the type of `A`, but simp doesn't get confused by -- them so for now we do not care. +-- xxx(grunweg): still correct? not verified @[simp] theorem coe_toLinear : (@toLinear n ‹_› ‹_› _ _ A : (n → R) →ₗ[R] n → R) = Matrix.mulVecLin A := rfl diff --git a/Mathlib/Logic/Embedding/Basic.lean b/Mathlib/Logic/Embedding/Basic.lean index fe14a4a049c64..5c26230c4a6c6 100644 --- a/Mathlib/Logic/Embedding/Basic.lean +++ b/Mathlib/Logic/Embedding/Basic.lean @@ -296,7 +296,8 @@ theorem coe_prodMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) rfl #align function.embedding.coe_prod_map Function.Embedding.coe_prodMap -/-- If `e₁` and `e₂` are embeddings, then so is `λ ⟨a, b⟩, ⟨e₁ a, e₂ b⟩ : PProd α γ → PProd β δ`. -/ +/-- If `e₁` and `e₂` are embeddings, + then so is `fun ⟨a, b⟩ ↦ ⟨e₁ a, e₂ b⟩ : PProd α γ → PProd β δ`. -/ def pprodMap {α β γ δ : Sort*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : PProd α γ ↪ PProd β δ := ⟨fun x => ⟨e₁ x.1, e₂ x.2⟩, e₁.injective.pprod_map e₂.injective⟩ #align function.embedding.pprod_map Function.Embedding.pprodMap diff --git a/Mathlib/MeasureTheory/Function/L2Space.lean b/Mathlib/MeasureTheory/Function/L2Space.lean index 62e53cc38981d..8ef3d8e8fbd4a 100644 --- a/Mathlib/MeasureTheory/Function/L2Space.lean +++ b/Mathlib/MeasureTheory/Function/L2Space.lean @@ -18,8 +18,8 @@ is also an inner product space, with inner product defined as `inner f g = ∫ a * `mem_L1_inner` : for `f` and `g` in `Lp E 2 μ`, the pointwise inner product `fun x ↦ ⟪f x, g x⟫` belongs to `Lp 𝕜 1 μ`. -* `integrable_inner` : for `f` and `g` in `Lp E 2 μ`, the pointwise inner product `λ x, ⟪f x, g x⟫` - is integrable. +* `integrable_inner` : for `f` and `g` in `Lp E 2 μ`, the pointwise inner product + `fun x ↦ ⟪f x, g x⟫` is integrable. * `L2.inner_product_space` : `Lp E 2 μ` is an inner product space. -/ diff --git a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean index 7df9ea4d19c30..b7effb1deb662 100644 --- a/Mathlib/MeasureTheory/Integral/CircleIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/CircleIntegral.lean @@ -293,8 +293,8 @@ theorem ContinuousOn.circleIntegrable {f : ℂ → E} {c : ℂ} {R : ℝ} (hR : ContinuousOn.circleIntegrable' <| (_root_.abs_of_nonneg hR).symm ▸ hf #align continuous_on.circle_integrable ContinuousOn.circleIntegrable -/-- The function `λ z, (z - w) ^ n`, `n : ℤ`, is circle integrable on the circle with center `c` and -radius `|R|` if and only if `R = 0` or `0 ≤ n`, or `w` does not belong to this circle. -/ +/-- The function `fun z ↦ (z - w) ^ n`, `n : ℤ`, is circle integrable on the circle with center `c` +and radius `|R|` if and only if `R = 0` or `0 ≤ n`, or `w` does not belong to this circle. -/ @[simp] theorem circleIntegrable_sub_zpow_iff {c w : ℂ} {R : ℝ} {n : ℤ} : CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| := by diff --git a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean index 11f0550b112bc..d6d75de3ecb64 100644 --- a/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean +++ b/Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean @@ -20,9 +20,10 @@ In this file we prove the Divergence theorem for Bochner integral on a box in Let `E` be a complete normed space. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is continuous on a rectangular box `[a, b] : Set ℝⁿ⁺¹`, `a ≤ b`, differentiable on its interior with -derivative `f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹`, and the divergence `λ x, ∑ i, f' x eᵢ i` is integrable on -`[a, b]`, where `eᵢ = Pi.single i 1` is the `i`-th basis vector, then its integral is equal to the -sum of integrals of `f` over the faces of `[a, b]`, taken with appropriate signs. Moreover, the same +derivative `f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹`, and the divergence `fun x ↦ ∑ i, f' x eᵢ i` +is integrable on `[a, b]`, where `eᵢ = Pi.single i 1` is the `i`-th basis vector, +then its integral is equal to the sum of integrals of `f` over the faces of `[a, b]`, +taken with appropriate signs. Moreover, the same is true if the function is not differentiable at countably many points of the interior of `[a, b]`. Once we prove the general theorem, we deduce corollaries for functions `ℝ → E` and pairs of diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean index 0fcdbc086d1ec..1492c4468c83f 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean @@ -51,7 +51,7 @@ open ContinuousMap /- The following lemma is a minor variation on `integrable_of_summable_norm_restrict` in `Mathlib/MeasureTheory/Integral/SetIntegral.lean`, but it is placed here because it needs to know that `Icc a b` has volume `b - a`. -/ -/-- If the sequence with `n`-th term the the sup norm of `λ x, f (x + n)` on the interval `Icc 0 1`, +/-- If the sequence with `n`-th term the the sup norm of `fun x ↦ f (x + n)` on the interval `Icc 0 1`, for `n ∈ ℤ`, is summable, then `f` is integrable on `ℝ`. -/ theorem Real.integrable_of_summable_norm_Icc {E : Type*} [NormedAddCommGroup E] {f : C(ℝ, E)} (hf : Summable fun n : ℤ => ‖(f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)‖) : diff --git a/Mathlib/ModelTheory/DirectLimit.lean b/Mathlib/ModelTheory/DirectLimit.lean index 2b08a42227b1e..72bf47612d904 100644 --- a/Mathlib/ModelTheory/DirectLimit.lean +++ b/Mathlib/ModelTheory/DirectLimit.lean @@ -40,13 +40,13 @@ variable (f : ∀ i j, i ≤ j → G i ↪[L] G j) namespace DirectedSystem /-- A copy of `DirectedSystem.map_self` specialized to `L`-embeddings, as otherwise the -`λ i j h, f i j h` can confuse the simplifier. -/ +`fun i j h ↦ f i j h` can confuse the simplifier. -/ nonrec theorem map_self [DirectedSystem G fun i j h => f i j h] (i x h) : f i i h x = x := DirectedSystem.map_self (fun i j h => f i j h) i x h #align first_order.language.directed_system.map_self FirstOrder.Language.DirectedSystem.map_self /-- A copy of `DirectedSystem.map_map` specialized to `L`-embeddings, as otherwise the -`λ i j h, f i j h` can confuse the simplifier. -/ +`fun i j h ↦ f i j h` can confuse the simplifier. -/ nonrec theorem map_map [DirectedSystem G fun i j h => f i j h] {i j k} (hij hjk x) : f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x := DirectedSystem.map_map (fun i j h => f i j h) hij hjk x diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean index d584fddde36ce..ae93b5ff142bf 100644 --- a/Mathlib/Order/Filter/AtTopBot.lean +++ b/Mathlib/Order/Filter/AtTopBot.lean @@ -1054,7 +1054,7 @@ variable [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r c : α} -/ -/-- If `r` is a positive constant, then `λ x, r * f x` tends to infinity along a filter if and only +/-- If `r` is a positive constant, then `fun x ↦ r * f x` tends to infinity along a filter if and only if `f` tends to infinity along the same filter. -/ theorem tendsto_const_mul_atTop_of_pos (hr : 0 < r) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop := @@ -1062,7 +1062,7 @@ theorem tendsto_const_mul_atTop_of_pos (hr : 0 < r) : Tendsto.atTop_of_const_mul (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne'] ⟩ #align filter.tendsto_const_mul_at_top_of_pos Filter.tendsto_const_mul_atTop_of_pos -/-- If `r` is a positive constant, then `λ x, f x * r` tends to infinity along a filter if and only +/-- If `r` is a positive constant, then `fun x ↦ f x * r` tends to infinity along a filter if and only if `f` tends to infinity along the same filter. -/ theorem tendsto_mul_const_atTop_of_pos (hr : 0 < r) : Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop := by @@ -1144,49 +1144,49 @@ section LinearOrderedField variable [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} -/-- If `r` is a positive constant, then `λ x, r * f x` tends to negative infinity along a filter if +/-- If `r` is a positive constant, then `fun x ↦ r * f x` tends to negative infinity along a filter if and only if `f` tends to negative infinity along the same filter. -/ theorem tendsto_const_mul_atBot_of_pos (hr : 0 < r) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot := by simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr #align filter.tendsto_const_mul_at_bot_of_pos Filter.tendsto_const_mul_atBot_of_pos -/-- If `r` is a positive constant, then `λ x, f x * r` tends to negative infinity along a filter if +/-- If `r` is a positive constant, then `fun x ↦f x * r` tends to negative infinity along a filter if and only if `f` tends to negative infinity along the same filter. -/ theorem tendsto_mul_const_atBot_of_pos (hr : 0 < r) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot := by simpa only [mul_comm] using tendsto_const_mul_atBot_of_pos hr #align filter.tendsto_mul_const_at_bot_of_pos Filter.tendsto_mul_const_atBot_of_pos -/-- If `r` is a negative constant, then `λ x, r * f x` tends to infinity along a filter if and only +/-- If `r` is a negative constant, then `fun x ↦r * f x` tends to infinity along a filter if and only if `f` tends to negative infinity along the same filter. -/ theorem tendsto_const_mul_atTop_of_neg (hr : r < 0) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot := by simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr) #align filter.tendsto_const_mul_at_top_of_neg Filter.tendsto_const_mul_atTop_of_neg -/-- If `r` is a negative constant, then `λ x, f x * r` tends to infinity along a filter if and only +/-- If `r` is a negative constant, then `fun x ↦f x * r` tends to infinity along a filter if and only if `f` tends to negative infinity along the same filter. -/ theorem tendsto_mul_const_atTop_of_neg (hr : r < 0) : Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot := by simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr #align filter.tendsto_mul_const_at_top_of_neg Filter.tendsto_mul_const_atTop_of_neg -/-- If `r` is a negative constant, then `λ x, r * f x` tends to negative infinity along a filter if +/-- If `r` is a negative constant, then `fun x ↦r * f x` tends to negative infinity along a filter if and only if `f` tends to infinity along the same filter. -/ theorem tendsto_const_mul_atBot_of_neg (hr : r < 0) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop := by simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr) #align filter.tendsto_const_mul_at_bot_of_neg Filter.tendsto_const_mul_atBot_of_neg -/-- If `r` is a negative constant, then `λ x, f x * r` tends to negative infinity along a filter if +/-- If `r` is a negative constant, then `fun x ↦f x * r` tends to negative infinity along a filter if and only if `f` tends to infinity along the same filter. -/ theorem tendsto_mul_const_atBot_of_neg (hr : r < 0) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop := by simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr #align filter.tendsto_mul_const_at_bot_of_neg Filter.tendsto_mul_const_atBot_of_neg -/-- The function `λ x, r * f x` tends to infinity along a nontrivial filter if and only if `r > 0` +/-- The function `fun x ↦ r * f x` tends to infinity along a nontrivial filter if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/ theorem tendsto_const_mul_atTop_iff [NeBot l] : Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by @@ -1196,21 +1196,21 @@ theorem tendsto_const_mul_atTop_iff [NeBot l] : · simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_pos] #align filter.tendsto_const_mul_at_top_iff Filter.tendsto_const_mul_atTop_iff -/-- The function `λ x, f x * r` tends to infinity along a nontrivial filter if and only if `r > 0` +/-- The function `fun x ↦ f x * r` tends to infinity along a nontrivial filter if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/ theorem tendsto_mul_const_atTop_iff [NeBot l] : Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by simp only [mul_comm _ r, tendsto_const_mul_atTop_iff] #align filter.tendsto_mul_const_at_top_iff Filter.tendsto_mul_const_atTop_iff -/-- The function `λ x, r * f x` tends to negative infinity along a nontrivial filter if and only if +/-- The function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/ theorem tendsto_const_mul_atBot_iff [NeBot l] : Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg] #align filter.tendsto_const_mul_at_bot_iff Filter.tendsto_const_mul_atBot_iff -/-- The function `λ x, f x * r` tends to negative infinity along a nontrivial filter if and only if +/-- The function `fun x ↦ f x * r` tends to negative infinity along a nontrivial filter if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/ theorem tendsto_mul_const_atBot_iff [NeBot l] : Tendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by diff --git a/Mathlib/Probability/Distributions/Poisson.lean b/Mathlib/Probability/Distributions/Poisson.lean index 7f356dadc5c60..4e7e7271eeeb8 100644 --- a/Mathlib/Probability/Distributions/Poisson.lean +++ b/Mathlib/Probability/Distributions/Poisson.lean @@ -14,7 +14,7 @@ import Mathlib.Probability.ProbabilityMassFunction.Basic Define the Poisson measure over the natural numbers ## Main definitions -* `poissonPMFReal`: the function `λ n ↦ exp (- λ) * λ ^ n / n!` +* `poissonPMFReal`: the function `fun n ↦ exp (- λ) * λ ^ n / n!` for `n ∈ ℕ`, which is the probability density function of a Poisson distribution with rate `λ > 0`. * `poissonPMF`: `ℝ≥0∞`-valued pdf, diff --git a/Mathlib/RingTheory/WittVector/IsPoly.lean b/Mathlib/RingTheory/WittVector/IsPoly.lean index c31f67830b0df..4c87b6e885481 100644 --- a/Mathlib/RingTheory/WittVector/IsPoly.lean +++ b/Mathlib/RingTheory/WittVector/IsPoly.lean @@ -266,7 +266,7 @@ instance IsPoly.comp₂ {g f} [hg : IsPoly p g] [hf : IsPoly₂ p f] : simp only [peval, aeval_bind₁, Function.comp, hg, hf] #align witt_vector.is_poly.comp₂ WittVector.IsPoly.comp₂ -/-- The diagonal `λ x, f x x` of a polynomial function `f` is polynomial. -/ +/-- The diagonal `fun x ↦f x x` of a polynomial function `f` is polynomial. -/ -- Porting note: made this an instance instance IsPoly₂.diag {f} [hf : IsPoly₂ p f] : IsPoly p fun R _Rcr x => f x x := by obtain ⟨φ, hf⟩ := hf diff --git a/Mathlib/Tactic/SimpRw.lean b/Mathlib/Tactic/SimpRw.lean index 5c3728ea44ce8..600ac1a279b5a 100644 --- a/Mathlib/Tactic/SimpRw.lean +++ b/Mathlib/Tactic/SimpRw.lean @@ -34,7 +34,7 @@ def withSimpRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) /-- `simp_rw` functions as a mix of `simp` and `rw`. Like `rw`, it applies each rewrite rule in the given order, but like `simp` it repeatedly applies these -rules and also under binders like `∀ x, ...`, `∃ x, ...` and `λ x, ...`. +rules and also under binders like `∀ x, ...`, `∃ x, ...` and `fun x ↦...`. Usage: - `simp_rw [lemma_1, ..., lemma_n]` will rewrite the goal by applying the diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean index 0c125c0f1b8a5..0d0983c5cb9da 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Ring.lean @@ -134,7 +134,7 @@ end DivisionSemiring ### Multipliying two infinite sums In this section, we prove various results about `(∑' x : ι, f x) * (∑' y : κ, g y)`. Note that we -always assume that the family `λ x : ι × κ, f x.1 * g x.2` is summable, since there is no way to +always assume that the family `fun x : ι × κ ↦ f x.1 * g x.2` is summable, since there is no way to deduce this from the summabilities of `f` and `g` in general, but if you are working in a normed space, you may want to use the analogous lemmas in `Analysis/NormedSpace/Basic` (e.g `tsum_mul_tsum_of_summable_norm`). diff --git a/Mathlib/Topology/Algebra/Polynomial.lean b/Mathlib/Topology/Algebra/Polynomial.lean index 690a498dc48f7..087dd7322f953 100644 --- a/Mathlib/Topology/Algebra/Polynomial.lean +++ b/Mathlib/Topology/Algebra/Polynomial.lean @@ -23,7 +23,7 @@ In this file we prove the following lemmas. * `Polynomial.continuous`: `Polynomial.eval` defines a continuous functions; we also prove convenience lemmas `Polynomial.continuousAt`, `Polynomial.continuousWithinAt`, `Polynomial.continuousOn`. -* `Polynomial.tendsto_norm_atTop`: `λ x, ‖Polynomial.eval (z x) p‖` tends to infinity provided that +* `Polynomial.tendsto_norm_atTop`: `fun x ↦‖Polynomial.eval (z x) p‖` tends to infinity provided that `fun x ↦ ‖z x‖` tends to infinity and `0 < degree p`; * `Polynomial.tendsto_abv_eval₂_atTop`, `Polynomial.tendsto_abv_atTop`, `Polynomial.tendsto_abv_aeval_atTop`: a few versions of the previous statement for diff --git a/Mathlib/Topology/Algebra/UniformMulAction.lean b/Mathlib/Topology/Algebra/UniformMulAction.lean index 0589b6053b916..e4f0d81c2796c 100644 --- a/Mathlib/Topology/Algebra/UniformMulAction.lean +++ b/Mathlib/Topology/Algebra/UniformMulAction.lean @@ -36,7 +36,7 @@ class UniformContinuousConstVAdd [VAdd M X] : Prop where uniformContinuous_const_vadd : ∀ c : M, UniformContinuous (c +ᵥ · : X → X) #align has_uniform_continuous_const_vadd UniformContinuousConstVAdd -/-- A multiplicative action such that for all `c`, the map `λ x, c • x` is uniformly continuous. -/ +/-- A multiplicative action such that for all `c`, the map `fun x ↦c • x` is uniformly continuous. -/ @[to_additive] class UniformContinuousConstSMul [SMul M X] : Prop where uniformContinuous_const_smul : ∀ c : M, UniformContinuous (c • · : X → X) diff --git a/Mathlib/Topology/Homotopy/HSpaces.lean b/Mathlib/Topology/Homotopy/HSpaces.lean index 794de152bdc1f..b293013dcae5a 100644 --- a/Mathlib/Topology/Homotopy/HSpaces.lean +++ b/Mathlib/Topology/Homotopy/HSpaces.lean @@ -16,7 +16,7 @@ This file defines H-spaces mainly following the approach proposed by Serre in hi *Homologie singulière des espaces fibrés*. The idea beneath `H-spaces` is that they are topological spaces with a binary operation `⋀ : X → X → X` that is a homotopic-theoretic weakening of an operation what would make `X` into a topological monoid. In particular, there exists a "neutral -element" `e : X` such that `λ x, e ⋀ x` and `λ x, x ⋀ e` are homotopic to the identity on `X`, see +element" `e : X` such that `fun x ↦e ⋀ x` and `fun x ↦x ⋀ e` are homotopic to the identity on `X`, see [the Wikipedia page of H-spaces](https://en.wikipedia.org/wiki/H-space). Some notable properties of `H-spaces` are @@ -35,7 +35,7 @@ equal to the product of `H-space` structures on `G` and `G'`. ## To Do * Prove that for every `NormedAddTorsor Z` and every `z : Z`, the operation -`λ x y, midpoint x y` defines an `H-space` structure with `z` as a "neutral element". +`fun x y ↦ midpoint x y` defines an `H-space` structure with `z` as a "neutral element". * Prove that `S^0`, `S^1`, `S^3` and `S^7` are the unique spheres that are `H-spaces`, where the first three inherit the structure because they are topological groups (they are Lie groups, actually), isomorphic to the invertible elements in `ℤ`, in `ℂ` and in the quaternion; and the diff --git a/test/Simps.lean b/test/Simps.lean index 177d14f2070e8..c0b25a935943c 100644 --- a/test/Simps.lean +++ b/test/Simps.lean @@ -612,9 +612,9 @@ noncomputable def Equiv.Simps.invFun (e : α ≃ β) : β → α := Classical.ch run_cmd liftTermElabM <| do successIfFail (getRawProjections .missing `FaultyManualCoercion.Equiv) -- "Invalid custom projection: --- λ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β), Classical.choice _ +-- fun {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) ↦ Classical.choice _ -- Expression is not definitionally equal to --- λ (α : Sort u_1) (β : Sort u_2) (x : α ≃ β), x.invFun" +-- fun (α : Sort u_1) (β : Sort u_2) (x : α ≃ β) ↦ x.invFun" end FaultyManualCoercion From 118fb287c2594a1e06b91f73708453609e116977 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 19 Feb 2024 19:24:31 +0100 Subject: [PATCH 2/3] Fix most line length warnings. --- Mathlib/Analysis/BoxIntegral/Basic.lean | 8 ++++---- Mathlib/Analysis/Complex/OpenMapping.lean | 4 ++-- Mathlib/Data/Matrix/Basic.lean | 4 ++-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean | 7 +++---- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean | 2 +- Mathlib/Topology/Algebra/Polynomial.lean | 4 ++-- Mathlib/Topology/Algebra/UniformMulAction.lean | 3 ++- Mathlib/Topology/Homotopy/HSpaces.lean | 5 +++-- 8 files changed, 19 insertions(+), 18 deletions(-) diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean index 0b42b7b169452..812612f78fc4c 100644 --- a/Mathlib/Analysis/BoxIntegral/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Basic.lean @@ -638,8 +638,8 @@ theorem tendsto_integralSum_sum_integral (h : Integrable I l f vol) (π₀ : Pre exact h.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq ε0 hc hU #align box_integral.integrable.tendsto_integral_sum_sum_integral BoxIntegral.Integrable.tendsto_integralSum_sum_integral -/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of `I`: -if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, then the sum of integrals +/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of +`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`. See also `BoxIntegral.Integrable.toBoxAdditive` for a bundled version. -/ @@ -651,8 +651,8 @@ theorem sum_integral_congr (h : Integrable I l f vol) {π₁ π₂ : Prepartitio exact h.tendsto_integralSum_sum_integral π₂ #align box_integral.integrable.sum_integral_congr BoxIntegral.Integrable.sum_integral_congr -/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of `I`: -if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, then the sum of integrals +/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of +`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`. See also `BoxIntegral.Integrable.sum_integral_congr` for an unbundled version. -/ diff --git a/Mathlib/Analysis/Complex/OpenMapping.lean b/Mathlib/Analysis/Complex/OpenMapping.lean index 11f005bdc8bd0..059f310f18f23 100644 --- a/Mathlib/Analysis/Complex/OpenMapping.lean +++ b/Mathlib/Analysis/Complex/OpenMapping.lean @@ -21,8 +21,8 @@ its image `f z₀`. The results extend in higher dimension to `g : E → ℂ`. The proof of the local version on `ℂ` goes through two main steps: first, assuming that the function is not constant around `z₀`, use the isolated zero principle to show that `‖f z‖` is bounded below on a small `sphere z₀ r` around `z₀`, and then use the maximum principle applied to the auxiliary -function `(fun z ↦ ‖f z - v‖)` to show that any `v` close enough to `f z₀` is in `f '' ball z₀ r`. That -second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`. +function `(fun z ↦ ‖f z - v‖)` to show that any `v` close enough to `f z₀` is in `f '' ball z₀ r`. +That second step is implemented in `DiffContOnCl.ball_subset_image_closedBall`. ## Main results diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean index 1463d784f21c2..943dca0da5fd4 100644 --- a/Mathlib/Data/Matrix/Basic.lean +++ b/Mathlib/Data/Matrix/Basic.lean @@ -41,8 +41,8 @@ The locale `Matrix` gives the following notation: For convenience, `Matrix m n α` is defined as `m → n → α`, as this allows elements of the matrix to be accessed with `A i j`. However, it is not advisable to _construct_ matrices using terms of the -form `fun i j ↦ _` or even `(fun i j ↦ _ : Matrix m n α)`, as these are not recognized by lean as having -the right type. Instead, `Matrix.of` should be used. +form `fun i j ↦ _` or even `(fun i j ↦ _ : Matrix m n α)`, as these are not recognized by Lean +as having the right type. Instead, `Matrix.of` should be used. ## TODO diff --git a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean index 47c851b8ff0aa..ba61470847cea 100644 --- a/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean +++ b/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup.lean @@ -128,11 +128,10 @@ def toLinear : GeneralLinearGroup n R ≃* LinearMap.GeneralLinearGroup R (n → Units.mapEquiv Matrix.toLinAlgEquiv'.toRingEquiv.toMulEquiv #align matrix.general_linear_group.to_linear Matrix.GeneralLinearGroup.toLinear --- Note that without the `@` and `‹_›`, lean infers `fun a b ↦ _inst a b` instead of `_inst` as the +-- Note that without the `@` and `‹_›`, Lean infers `fun a b ↦ _inst a b` instead of `_inst` as the -- decidability argument, which prevents `simp` from obtaining the instance by unification. --- These `fun a b ↦ _inst a b` terms also appear in the type of `A`, but simp doesn't get confused by --- them so for now we do not care. --- xxx(grunweg): still correct? not verified +-- These `fun a b ↦ _inst a b` terms also appear in the type of `A`, but simp doesn't get confused +-- by them so for now we do not care. @[simp] theorem coe_toLinear : (@toLinear n ‹_› ‹_› _ _ A : (n → R) →ₗ[R] n → R) = Matrix.mulVecLin A := rfl diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean index 1492c4468c83f..90720a3b306b7 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean @@ -51,7 +51,7 @@ open ContinuousMap /- The following lemma is a minor variation on `integrable_of_summable_norm_restrict` in `Mathlib/MeasureTheory/Integral/SetIntegral.lean`, but it is placed here because it needs to know that `Icc a b` has volume `b - a`. -/ -/-- If the sequence with `n`-th term the the sup norm of `fun x ↦ f (x + n)` on the interval `Icc 0 1`, +/-- If the sequence with `n`-th term the sup norm of `fun x ↦ f (x + n)` on the interval `Icc 0 1`, for `n ∈ ℤ`, is summable, then `f` is integrable on `ℝ`. -/ theorem Real.integrable_of_summable_norm_Icc {E : Type*} [NormedAddCommGroup E] {f : C(ℝ, E)} (hf : Summable fun n : ℤ => ‖(f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)‖) : diff --git a/Mathlib/Topology/Algebra/Polynomial.lean b/Mathlib/Topology/Algebra/Polynomial.lean index 087dd7322f953..9d5a18d39ddd9 100644 --- a/Mathlib/Topology/Algebra/Polynomial.lean +++ b/Mathlib/Topology/Algebra/Polynomial.lean @@ -23,8 +23,8 @@ In this file we prove the following lemmas. * `Polynomial.continuous`: `Polynomial.eval` defines a continuous functions; we also prove convenience lemmas `Polynomial.continuousAt`, `Polynomial.continuousWithinAt`, `Polynomial.continuousOn`. -* `Polynomial.tendsto_norm_atTop`: `fun x ↦‖Polynomial.eval (z x) p‖` tends to infinity provided that - `fun x ↦ ‖z x‖` tends to infinity and `0 < degree p`; +* `Polynomial.tendsto_norm_atTop`: `fun x ↦‖Polynomial.eval (z x) p‖` tends to infinity + provided that `fun x ↦ ‖z x‖` tends to infinity and `0 < degree p`; * `Polynomial.tendsto_abv_eval₂_atTop`, `Polynomial.tendsto_abv_atTop`, `Polynomial.tendsto_abv_aeval_atTop`: a few versions of the previous statement for `IsAbsoluteValue abv` instead of norm. diff --git a/Mathlib/Topology/Algebra/UniformMulAction.lean b/Mathlib/Topology/Algebra/UniformMulAction.lean index e4f0d81c2796c..a5599bda7e3e1 100644 --- a/Mathlib/Topology/Algebra/UniformMulAction.lean +++ b/Mathlib/Topology/Algebra/UniformMulAction.lean @@ -36,7 +36,8 @@ class UniformContinuousConstVAdd [VAdd M X] : Prop where uniformContinuous_const_vadd : ∀ c : M, UniformContinuous (c +ᵥ · : X → X) #align has_uniform_continuous_const_vadd UniformContinuousConstVAdd -/-- A multiplicative action such that for all `c`, the map `fun x ↦c • x` is uniformly continuous. -/ +/-- A multiplicative action such that for all `c`, +the map `fun x ↦c • x` is uniformly continuous. -/ @[to_additive] class UniformContinuousConstSMul [SMul M X] : Prop where uniformContinuous_const_smul : ∀ c : M, UniformContinuous (c • · : X → X) diff --git a/Mathlib/Topology/Homotopy/HSpaces.lean b/Mathlib/Topology/Homotopy/HSpaces.lean index b293013dcae5a..13e23f707de48 100644 --- a/Mathlib/Topology/Homotopy/HSpaces.lean +++ b/Mathlib/Topology/Homotopy/HSpaces.lean @@ -15,8 +15,9 @@ import Mathlib.Topology.Homotopy.Basic This file defines H-spaces mainly following the approach proposed by Serre in his paper *Homologie singulière des espaces fibrés*. The idea beneath `H-spaces` is that they are topological spaces with a binary operation `⋀ : X → X → X` that is a homotopic-theoretic weakening of an -operation what would make `X` into a topological monoid. In particular, there exists a "neutral -element" `e : X` such that `fun x ↦e ⋀ x` and `fun x ↦x ⋀ e` are homotopic to the identity on `X`, see +operation what would make `X` into a topological monoid. +In particular, there exists a "neutral element" `e : X` such that `fun x ↦e ⋀ x` and +`fun x ↦x ⋀ e` are homotopic to the identity on `X`, see [the Wikipedia page of H-spaces](https://en.wikipedia.org/wiki/H-space). Some notable properties of `H-spaces` are From 8ea772e54ffdce3430cbc911aecacb97af6cf44f Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Mon, 19 Feb 2024 19:25:23 +0100 Subject: [PATCH 3/3] doc(Filter/AtTopBot): fix line length; tweak docstrings - Instead of repeating 'a function' or 'the same filter', name it. - Use semantic linebreaking slightly more: it's more robust long-term, and I have to touch these lines anyway. - Edit nearby docstrings for consistency. (Happy to revert that part.) --- Mathlib/Order/Filter/AtTopBot.lean | 116 ++++++++++++++--------------- 1 file changed, 58 insertions(+), 58 deletions(-) diff --git a/Mathlib/Order/Filter/AtTopBot.lean b/Mathlib/Order/Filter/AtTopBot.lean index ae93b5ff142bf..8814f430c52d2 100644 --- a/Mathlib/Order/Filter/AtTopBot.lean +++ b/Mathlib/Order/Filter/AtTopBot.lean @@ -1054,29 +1054,29 @@ variable [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r c : α} -/ -/-- If `r` is a positive constant, then `fun x ↦ r * f x` tends to infinity along a filter if and only -if `f` tends to infinity along the same filter. -/ +/-- If `r` is a positive constant, `fun x ↦ r * f x` tends to infinity along a filter +if and only if `f` tends to infinity along the same filter. -/ theorem tendsto_const_mul_atTop_of_pos (hr : 0 < r) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atTop := ⟨fun h => h.atTop_of_const_mul hr, fun h => Tendsto.atTop_of_const_mul (inv_pos.2 hr) <| by simpa only [inv_mul_cancel_left₀ hr.ne'] ⟩ #align filter.tendsto_const_mul_at_top_of_pos Filter.tendsto_const_mul_atTop_of_pos -/-- If `r` is a positive constant, then `fun x ↦ f x * r` tends to infinity along a filter if and only -if `f` tends to infinity along the same filter. -/ +/-- If `r` is a positive constant, `fun x ↦ f x * r` tends to infinity along a filter +if and only if `f` tends to infinity along the same filter. -/ theorem tendsto_mul_const_atTop_of_pos (hr : 0 < r) : Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop := by simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr #align filter.tendsto_mul_const_at_top_of_pos Filter.tendsto_mul_const_atTop_of_pos -/-- If `r` is a positive constant, then `x ↦ f x / r` tends to infinity along a filter if and only -if `f` tends to infinity along the same filter. -/ +/-- If `r` is a positive constant, `x ↦ f x / r` tends to infinity along a filter +if and only if `f` tends to infinity along the same filter. -/ lemma tendsto_div_const_atTop_of_pos (hr : 0 < r) : Tendsto (λ x ↦ f x / r) l atTop ↔ Tendsto f l atTop := by simpa only [div_eq_mul_inv] using tendsto_mul_const_atTop_of_pos (inv_pos.2 hr) -/-- If `f` tends to infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to infinity -if and only if `0 < r. `-/ +/-- If `f` tends to infinity along a nontrivial filter `l`, then +`fun x ↦ r * f x` tends to infinity if and only if `0 < r. `-/ theorem tendsto_const_mul_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atTop ↔ 0 < r := by refine' ⟨fun hrf => not_le.mp fun hr => _, fun hr => (tendsto_const_mul_atTop_of_pos hr).mpr h⟩ @@ -1084,20 +1084,20 @@ theorem tendsto_const_mul_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) : exact (mul_nonpos_of_nonpos_of_nonneg hr hx).not_lt hrx #align filter.tendsto_const_mul_at_top_iff_pos Filter.tendsto_const_mul_atTop_iff_pos -/-- If `f` tends to infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to infinity -if and only if `0 < r. `-/ +/-- If `f` tends to infinity along a nontrivial filter `l`, then +`fun x ↦ f x * r` tends to infinity if and only if `0 < r. `-/ theorem tendsto_mul_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atTop ↔ 0 < r := by simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h] #align filter.tendsto_mul_const_at_top_iff_pos Filter.tendsto_mul_const_atTop_iff_pos -/-- If `f` tends to infinity along a nontrivial filter `l`, then `x ↦ f x * r` tends to infinity -if and only if `0 < r. `-/ +/-- If `f` tends to infinity along a nontrivial filter `l`, then +`x ↦ f x * r` tends to infinity if and only if `0 < r. `-/ lemma tendsto_div_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) : Tendsto (λ x ↦ f x / r) l atTop ↔ 0 < r := by simp only [div_eq_mul_inv, tendsto_mul_const_atTop_iff_pos h, inv_pos] -/-- If a function tends to infinity along a filter, then this function multiplied by a positive +/-- If `f` tends to infinity along a filter, then `f` multiplied by a positive constant (on the left) also tends to infinity. For a version working in `ℕ` or `ℤ`, use `filter.tendsto.const_mul_atTop'` instead. -/ theorem Tendsto.const_mul_atTop (hr : 0 < r) (hf : Tendsto f l atTop) : @@ -1105,7 +1105,7 @@ theorem Tendsto.const_mul_atTop (hr : 0 < r) (hf : Tendsto f l atTop) : (tendsto_const_mul_atTop_of_pos hr).2 hf #align filter.tendsto.const_mul_at_top Filter.Tendsto.const_mul_atTop -/-- If a function tends to infinity along a filter, then this function multiplied by a positive +/-- If a function `f` tends to infinity along a filter, then `f` multiplied by a positive constant (on the right) also tends to infinity. For a version working in `ℕ` or `ℤ`, use `filter.tendsto.atTop_mul_const'` instead. -/ theorem Tendsto.atTop_mul_const (hr : 0 < r) (hf : Tendsto f l atTop) : @@ -1113,7 +1113,7 @@ theorem Tendsto.atTop_mul_const (hr : 0 < r) (hf : Tendsto f l atTop) : (tendsto_mul_const_atTop_of_pos hr).2 hf #align filter.tendsto.at_top_mul_const Filter.Tendsto.atTop_mul_const -/-- If a function tends to infinity along a filter, then this function divided by a positive +/-- If a function `f` tends to infinity along a filter, then `f` divided by a positive constant also tends to infinity. -/ theorem Tendsto.atTop_div_const (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x / r) l atTop := by @@ -1144,50 +1144,50 @@ section LinearOrderedField variable [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} -/-- If `r` is a positive constant, then `fun x ↦ r * f x` tends to negative infinity along a filter if -and only if `f` tends to negative infinity along the same filter. -/ +/-- If `r` is a positive constant, `fun x ↦ r * f x` tends to negative infinity along a filter +if and only if `f` tends to negative infinity along the same filter. -/ theorem tendsto_const_mul_atBot_of_pos (hr : 0 < r) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot := by simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr #align filter.tendsto_const_mul_at_bot_of_pos Filter.tendsto_const_mul_atBot_of_pos -/-- If `r` is a positive constant, then `fun x ↦f x * r` tends to negative infinity along a filter if -and only if `f` tends to negative infinity along the same filter. -/ +/-- If `r` is a positive constant, `fun x ↦f x * r` tends to negative infinity along a filter +if and only if `f` tends to negative infinity along the same filter. -/ theorem tendsto_mul_const_atBot_of_pos (hr : 0 < r) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atBot := by simpa only [mul_comm] using tendsto_const_mul_atBot_of_pos hr #align filter.tendsto_mul_const_at_bot_of_pos Filter.tendsto_mul_const_atBot_of_pos -/-- If `r` is a negative constant, then `fun x ↦r * f x` tends to infinity along a filter if and only -if `f` tends to negative infinity along the same filter. -/ +/-- If `r` is a negative constant, `fun x ↦r * f x` tends to infinity along a filter `l` +if and only if `f` tends to negative infinity along `l`. -/ theorem tendsto_const_mul_atTop_of_neg (hr : r < 0) : Tendsto (fun x => r * f x) l atTop ↔ Tendsto f l atBot := by simpa only [neg_mul, tendsto_neg_atBot_iff] using tendsto_const_mul_atBot_of_pos (neg_pos.2 hr) #align filter.tendsto_const_mul_at_top_of_neg Filter.tendsto_const_mul_atTop_of_neg -/-- If `r` is a negative constant, then `fun x ↦f x * r` tends to infinity along a filter if and only -if `f` tends to negative infinity along the same filter. -/ +/-- If `r` is a negative constant, `fun x ↦f x * r` tends to infinity along a filter `l` +if and only if `f` tends to negative infinity along `l`. -/ theorem tendsto_mul_const_atTop_of_neg (hr : r < 0) : Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot := by simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr #align filter.tendsto_mul_const_at_top_of_neg Filter.tendsto_mul_const_atTop_of_neg -/-- If `r` is a negative constant, then `fun x ↦r * f x` tends to negative infinity along a filter if -and only if `f` tends to infinity along the same filter. -/ +/-- If `r` is a negative constant, `fun x ↦r * f x` tends to negative infinity along a filter `l` +if and only if `f` tends to infinity along `l`. -/ theorem tendsto_const_mul_atBot_of_neg (hr : r < 0) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop := by simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr) #align filter.tendsto_const_mul_at_bot_of_neg Filter.tendsto_const_mul_atBot_of_neg -/-- If `r` is a negative constant, then `fun x ↦f x * r` tends to negative infinity along a filter if -and only if `f` tends to infinity along the same filter. -/ +/-- If `r` is a negative constant, `fun x ↦f x * r` tends to negative infinity along a filter `l` +if and only if `f` tends to infinity along `l`. -/ theorem tendsto_mul_const_atBot_of_neg (hr : r < 0) : Tendsto (fun x => f x * r) l atBot ↔ Tendsto f l atTop := by simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr #align filter.tendsto_mul_const_at_bot_of_neg Filter.tendsto_mul_const_atBot_of_neg -/-- The function `fun x ↦ r * f x` tends to infinity along a nontrivial filter if and only if `r > 0` -and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/ +/-- The function `fun x ↦ r * f x` tends to infinity along a nontrivial filter +if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/ theorem tendsto_const_mul_atTop_iff [NeBot l] : Tendsto (fun x => r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by rcases lt_trichotomy r 0 with (hr | rfl | hr) @@ -1196,113 +1196,113 @@ theorem tendsto_const_mul_atTop_iff [NeBot l] : · simp [hr, hr.not_lt, tendsto_const_mul_atTop_of_pos] #align filter.tendsto_const_mul_at_top_iff Filter.tendsto_const_mul_atTop_iff -/-- The function `fun x ↦ f x * r` tends to infinity along a nontrivial filter if and only if `r > 0` -and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/ +/-- The function `fun x ↦ f x * r` tends to infinity along a nontrivial filter +if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity. -/ theorem tendsto_mul_const_atTop_iff [NeBot l] : Tendsto (fun x => f x * r) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot := by simp only [mul_comm _ r, tendsto_const_mul_atTop_iff] #align filter.tendsto_mul_const_at_top_iff Filter.tendsto_mul_const_atTop_iff -/-- The function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter if and only if -`r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/ +/-- The function `fun x ↦ r * f x` tends to negative infinity along a nontrivial filter +if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/ theorem tendsto_const_mul_atBot_iff [NeBot l] : Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg] #align filter.tendsto_const_mul_at_bot_iff Filter.tendsto_const_mul_atBot_iff -/-- The function `fun x ↦ f x * r` tends to negative infinity along a nontrivial filter if and only if -`r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/ +/-- The function `fun x ↦ f x * r` tends to negative infinity along a nontrivial filter +if and only if `r > 0` and `f` tends to negative infinity or `r < 0` and `f` tends to infinity. -/ theorem tendsto_mul_const_atBot_iff [NeBot l] : Tendsto (fun x => f x * r) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop := by simp only [mul_comm _ r, tendsto_const_mul_atBot_iff] #align filter.tendsto_mul_const_at_bot_iff Filter.tendsto_mul_const_atBot_iff -/-- If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to -infinity if and only if `r < 0. `-/ +/-- If `f` tends to negative infinity along a nontrivial filter `l`, +then `fun x ↦ r * f x` tends to infinity if and only if `r < 0. `-/ theorem tendsto_const_mul_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atTop ↔ r < 0 := by simp [tendsto_const_mul_atTop_iff, h, h.not_tendsto disjoint_atBot_atTop] #align filter.tendsto_const_mul_at_top_iff_neg Filter.tendsto_const_mul_atTop_iff_neg -/-- If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to -infinity if and only if `r < 0. `-/ +/-- If `f` tends to negative infinity along a nontrivial filter `l`, +then `fun x ↦ f x * r` tends to infinity if and only if `r < 0. `-/ theorem tendsto_mul_const_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop ↔ r < 0 := by simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_neg h] #align filter.tendsto_mul_const_at_top_iff_neg Filter.tendsto_mul_const_atTop_iff_neg -/-- If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to -negative infinity if and only if `0 < r. `-/ +/-- If `f` tends to negative infinity along a nontrivial filter `l`, then +`fun x ↦ r * f x` tends to negative infinity if and only if `0 < r. `-/ theorem tendsto_const_mul_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atBot ↔ 0 < r := by simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop] #align filter.tendsto_const_mul_at_bot_iff_pos Filter.tendsto_const_mul_atBot_iff_pos -/-- If `f` tends to negative infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to -negative infinity if and only if `0 < r. `-/ +/-- If `f` tends to negative infinity along a nontrivial filter `l`, then +`fun x ↦ f x * r` tends to negative infinity if and only if `0 < r. `-/ theorem tendsto_mul_const_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atBot ↔ 0 < r := by simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_pos h] #align filter.tendsto_mul_const_at_bot_iff_pos Filter.tendsto_mul_const_atBot_iff_pos -/-- If `f` tends to infinity along a nontrivial filter `l`, then `fun x ↦ r * f x` tends to negative -infinity if and only if `r < 0. `-/ +/-- If `f` tends to infinity along a nontrivial filter, +`fun x ↦ r * f x` tends to negative infinity if and only if `r < 0. `-/ theorem tendsto_const_mul_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atBot ↔ r < 0 := by simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot] #align filter.tendsto_const_mul_at_bot_iff_neg Filter.tendsto_const_mul_atBot_iff_neg -/-- If `f` tends to infinity along a nontrivial filter `l`, then `fun x ↦ f x * r` tends to negative -infinity if and only if `r < 0. `-/ +/-- If `f` tends to infinity along a nontrivial filter, +`fun x ↦ f x * r` tends to negative infinity if and only if `r < 0. `-/ theorem tendsto_mul_const_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atBot ↔ r < 0 := by simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h] #align filter.tendsto_mul_const_at_bot_iff_neg Filter.tendsto_mul_const_atBot_iff_neg -/-- If a function tends to infinity along a filter, then this function multiplied by a negative -constant (on the left) tends to negative infinity. -/ +/-- If a function `f` tends to infinity along a filter, +then `f` multiplied by a negative constant (on the left) tends to negative infinity. -/ theorem Tendsto.neg_const_mul_atTop (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atBot := (tendsto_const_mul_atBot_of_neg hr).2 hf #align filter.tendsto.neg_const_mul_at_top Filter.Tendsto.neg_const_mul_atTop -/-- If a function tends to infinity along a filter, then this function multiplied by a negative -constant (on the right) tends to negative infinity. -/ +/-- If a function `f` tends to infinity along a filter, +then `f` multiplied by a negative constant (on the right) tends to negative infinity. -/ theorem Tendsto.atTop_mul_neg_const (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atBot := (tendsto_mul_const_atBot_of_neg hr).2 hf #align filter.tendsto.at_top_mul_neg_const Filter.Tendsto.atTop_mul_neg_const -/-- If a function tends to negative infinity along a filter, then this function multiplied by +/-- If a function `f` tends to negative infinity along a filter, then `f` multiplied by a positive constant (on the left) also tends to negative infinity. -/ theorem Tendsto.const_mul_atBot (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atBot := (tendsto_const_mul_atBot_of_pos hr).2 hf #align filter.tendsto.const_mul_at_bot Filter.Tendsto.const_mul_atBot -/-- If a function tends to negative infinity along a filter, then this function multiplied by +/-- If a function `f` tends to negative infinity along a filter, then `f` multiplied by a positive constant (on the right) also tends to negative infinity. -/ theorem Tendsto.atBot_mul_const (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atBot := (tendsto_mul_const_atBot_of_pos hr).2 hf #align filter.tendsto.at_bot_mul_const Filter.Tendsto.atBot_mul_const -/-- If a function tends to negative infinity along a filter, then this function divided by +/-- If a function `f` tends to negative infinity along a filter, then `f` divided by a positive constant also tends to negative infinity. -/ theorem Tendsto.atBot_div_const (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x / r) l atBot := by simpa only [div_eq_mul_inv] using hf.atBot_mul_const (inv_pos.2 hr) #align filter.tendsto.at_bot_div_const Filter.Tendsto.atBot_div_const -/-- If a function tends to negative infinity along a filter, then this function multiplied by -a negative constant (on the left) tends to positive infinity. -/ +/-- If a function `f` tends to negative infinity along a filter, +then `f` multiplied by a negative constant (on the left) tends to positive infinity. -/ theorem Tendsto.neg_const_mul_atBot (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => r * f x) l atTop := (tendsto_const_mul_atTop_of_neg hr).2 hf #align filter.tendsto.neg_const_mul_at_bot Filter.Tendsto.neg_const_mul_atBot -/-- If a function tends to negative infinity along a filter, then this function multiplied by -a negative constant (on the right) tends to positive infinity. -/ +/-- If a function tends to negative infinity along a filter, +then `f` multiplied by a negative constant (on the right) tends to positive infinity. -/ theorem Tendsto.atBot_mul_neg_const (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop := (tendsto_mul_const_atTop_of_neg hr).2 hf