Commit 2023-08-09 19:01 22d431c3

View on Github →

feat(Analysis/LocallyConvex/WithSeminorms): equicontinuity criteria (#5580)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup

added theorem WithSeminorms.uniformEquicontinuous_iff_exists_continuous_seminorm

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

added theorem ContinuousLinearMap.op_norm_le_iff

Modified Mathlib/Analysis/Seminorm.lean

added theorem Seminorm.bddAbove_of_absorbent

Modified Mathlib/Data/Real/ENNReal.lean

added theorem ENNReal.iSup_coe_eq_top

added theorem ENNReal.iSup_coe_lt_top

Modified Mathlib/Topology/Algebra/UniformGroup.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

modified theorem uniformContinuous_iInf_rng

modified theorem uniformContinuous_sInf_rng

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean

added theorem equicontinuousAt_empty

added theorem equicontinuousAt_iInf_dom

added theorem equicontinuousAt_iInf_rng

added theorem equicontinuous_empty

added theorem equicontinuous_iInf_dom

added theorem equicontinuous_iInf_rng

added theorem uniformEquicontinuous_empty

added theorem uniformEquicontinuous_iInf_rng

added theorem uniform_equicontinuous_infi_dom