Theorem Function.Periodic.compact_of_continuous'

Modification history

2024-06-28 09:13

Mathlib/Topology/Instances/Real.lean

chore(*): remove some deprecated theorems (#14214)

Deleted Function.Periodic.compact_of_continuous'View on Github →

2023-03-06 08:38

Mathlib/Topology/Instances/Real.lean

feat: port Topology.Instances.Real (#2633) …

Added Function.Periodic.compact_of_continuous'View on Github →