Commit 2023-02-11 08:36 e8599072

View on Github →

feat: Port Data.Real.Pointwise (#2196) Comments and stylish changes only.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/Pointwise.lean

added theorem Real.infᵢ_mul_of_nonneg

added theorem Real.infᵢ_mul_of_nonpos

added theorem Real.infₛ_smul_of_nonneg

added theorem Real.infₛ_smul_of_nonpos

added theorem Real.mul_infᵢ_of_nonneg

added theorem Real.mul_infᵢ_of_nonpos

added theorem Real.mul_supᵢ_of_nonneg

added theorem Real.mul_supᵢ_of_nonpos

added theorem Real.smul_infᵢ_of_nonneg

added theorem Real.smul_infᵢ_of_nonpos

added theorem Real.smul_supᵢ_of_nonneg

added theorem Real.smul_supᵢ_of_nonpos

added theorem Real.supᵢ_mul_of_nonneg

added theorem Real.supᵢ_mul_of_nonpos

added theorem Real.supₛ_smul_of_nonneg

added theorem Real.supₛ_smul_of_nonpos