Topological properties of ℝ #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
instTopologicalDivisionRingRealInstDivisionRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace :
Equations
- One or more equations did not get rendered due to their size.
theorem
Real.isTopologicalBasis_Ioo_rat :
TopologicalSpace.IsTopologicalBasis (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
@[deprecated HasContinuousInv₀.continuousAt_inv₀]
@[deprecated Continuous.inv₀]
theorem
Real.Continuous.inv
{α : Type u}
[TopologicalSpace α]
{f : α → ℝ}
(h : ∀ (a : α), f a ≠ 0)
(hf : Continuous f)
:
Continuous fun a => (f a)⁻¹
theorem
Real.isBounded_iff_bddBelow_bddAbove
{s : Set ℝ}
:
Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
theorem
Function.Periodic.compact_of_continuous
{α : Type u}
[TopologicalSpace α]
{f : ℝ → α}
{c : ℝ}
(hp : Function.Periodic f c)
(hc : c ≠ 0)
(hf : Continuous f)
:
A continuous, periodic function has compact range.
@[deprecated Function.Periodic.compact_of_continuous]
theorem
Function.Periodic.compact_of_continuous'
{α : Type u}
[TopologicalSpace α]
{f : ℝ → α}
{c : ℝ}
(hp : Function.Periodic f c)
(hc : 0 < c)
(hf : Continuous f)
:
theorem
Function.Periodic.isBounded_of_continuous
{α : Type u}
[PseudoMetricSpace α]
{f : ℝ → α}
{c : ℝ}
(hp : Function.Periodic f c)
(hc : c ≠ 0)
(hf : Continuous f)
:
A continuous, periodic function is bounded.
instance
Int.instDiscreteTopologySubtypeRealMemAddSubgroupInstAddGroupRealInstMembershipInstSetLikeAddSubgroupZmultiplesInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpacePseudoMetricSpace
{a : ℝ}
:
DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
This is a special case of NormedSpace.discreteTopology_zmultiples
. It exists only to simplify
dependencies.
Equations
- One or more equations did not get rendered due to their size.
Under the coercion from ℤ
to ℝ
, inverse images of compact sets are finite.
theorem
Int.tendsto_zmultiplesHom_cofinite
{a : ℝ}
(ha : a ≠ 0)
:
Filter.Tendsto (↑(↑(zmultiplesHom ℝ) a)) Filter.cofinite (Filter.cocompact ℝ)
For nonzero a
, the "multiples of a
" map zmultiplesHom
from ℤ
to ℝ
is discrete, i.e.
inverse images of compact sets are finite.
theorem
AddSubgroup.tendsto_zmultiples_subtype_cofinite
(a : ℝ)
:
Filter.Tendsto (↑(AddSubgroup.subtype (AddSubgroup.zmultiples a))) Filter.cofinite (Filter.cocompact ℝ)
The subgroup "multiples of a
" (zmultiples a
) is a discrete subgroup of ℝ
, i.e. its
intersection with compact sets is finite.