Topological properties of ℝ #
@[protected, instance]
theorem
real.continuous.inv
{α : Type u}
[topological_space α]
{f : α → ℝ}
(h : ∀ (a : α), f a ≠ 0)
(hf : continuous f) :
continuous (λ (a : α), (f a)⁻¹)
theorem
real.bounded_iff_bdd_below_bdd_above
{s : set ℝ} :
metric.bounded s ↔ bdd_below s ∧ bdd_above s
theorem
real.subset_Icc_Inf_Sup_of_bounded
{s : set ℝ}
(h : metric.bounded s) :
s ⊆ set.Icc (has_Inf.Inf s) (has_Sup.Sup s)
theorem
function.periodic.compact_of_continuous'
{α : Type u}
[topological_space α]
{f : ℝ → α}
{c : ℝ}
(hp : function.periodic f c)
(hc : 0 < c)
(hf : continuous f) :
is_compact (set.range f)
theorem
function.periodic.compact_of_continuous
{α : Type u}
[topological_space α]
{f : ℝ → α}
{c : ℝ}
(hp : function.periodic f c)
(hc : c ≠ 0)
(hf : continuous f) :
is_compact (set.range f)
A continuous, periodic function has compact range.
theorem
function.periodic.bounded_of_continuous
{α : Type u}
[pseudo_metric_space α]
{f : ℝ → α}
{c : ℝ}
(hp : function.periodic f c)
(hc : c ≠ 0)
(hf : continuous f) :
A continuous, periodic function is bounded.
Subgroups of ℝ
are either dense or cyclic. See real.subgroup_dense_of_no_min
and
subgroup_cyclic_of_min
for more precise statements.