Topological properties of ℝ

instance instNoncompactSpaceReal : NoncompactSpace ℝ

Equations

• instNoncompactSpaceReal = ⋯

theorem Real.uniformContinuous_add : UniformContinuous fun (p : ℝ × ℝ) => p.1 + p.2

theorem Real.uniformContinuous_neg : UniformContinuous Neg.neg

instance instContinuousStarReal : ContinuousStar ℝ

Equations

• instContinuousStarReal = ⋯

instance instUniformAddGroupReal : UniformAddGroup ℝ

Equations

• instUniformAddGroupReal = ⋯

instance instTopologicalAddGroupReal : TopologicalAddGroup ℝ

Equations

• instTopologicalAddGroupReal = ⋯

instance instTopologicalRingReal : TopologicalRing ℝ

Equations

• instTopologicalRingReal = ⋯

instance instTopologicalDivisionRingReal : TopologicalDivisionRing ℝ

Equations

• instTopologicalDivisionRingReal = ⋯

instance instProperSpaceReal : ProperSpace ℝ

Equations

• instProperSpaceReal = ⋯

instance instSecondCountableTopologyReal : SecondCountableTopology ℝ

Equations

• instSecondCountableTopologyReal = ⋯

theorem Real.isTopologicalBasis_Ioo_rat : TopologicalSpace.IsTopologicalBasis (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})

@[simp]

theorem Real.cobounded_eq : Bornology.cobounded ℝ = Filter.atBot ⊔ Filter.atTop

@[deprecated cocompact_eq_atBot_atTop]

theorem Real.cocompact_eq {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMaxOrder α] [NoMinOrder α] [OrderClosedTopology α] [CompactIccSpace α] : Filter.cocompact α = Filter.atBot ⊔ Filter.atTop

Alias of cocompact_eq_atBot_atTop.

@[deprecated atBot_le_cocompact]

theorem Real.atBot_le_cocompact {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMinOrder α] [ClosedIicTopology α] : Filter.atBot ≤ Filter.cocompact α

Alias of atBot_le_cocompact.

@[deprecated atTop_le_cocompact]

theorem Real.atTop_le_cocompact {α : Type u_2} [LinearOrder α] [TopologicalSpace α] [NoMaxOrder α] [ClosedIciTopology α] : Filter.atTop ≤ Filter.cocompact α

Alias of atTop_le_cocompact.

theorem Real.mem_closure_iff {s : Set ℝ} {x : ℝ} : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε

theorem Real.uniformContinuous_inv (s : Set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ x ∈ s, r ≤ |x|) : UniformContinuous fun (p : ↑s) => (↑p)⁻¹

theorem Real.uniformContinuous_abs : UniformContinuous abs

theorem Real.continuous_inv : Continuous fun (a : { r : ℝ // r ≠ 0 }) => (↑a)⁻¹

theorem Real.uniformContinuous_const_mul {x : ℝ} : UniformContinuous fun (x_1 : ℝ) => x * x_1

theorem Real.uniformContinuous_mul (s : Set (ℝ × ℝ)) {r₁ : ℝ} {r₂ : ℝ} (H : ∀ x ∈ s, |x.1| < r₁ ∧ |x.2| < r₂) : UniformContinuous fun (p : ↑s) => (↑p).1 * (↑p).2

instance Real.instCompleteSpace : CompleteSpace ℝ

Equations

• Real.instCompleteSpace = ⋯

theorem Real.totallyBounded_ball (x : ℝ) (ε : ℝ) : TotallyBounded (Metric.ball x ε)

theorem closure_of_rat_image_lt {q : ℚ} : closure (Rat.cast '' {x : ℚ | q < x}) = {r : ℝ | ↑q ≤ r}

instance instIsOrderBornology : IsOrderBornology ℝ

Equations

• instIsOrderBornology = ⋯

theorem Function.Periodic.compact_of_continuous {α : Type u} [TopologicalSpace α] {f : ℝ → α} {c : ℝ} (hp : Function.Periodic f c) (hc : c ≠ 0) (hf : Continuous f) : IsCompact (Set.range f)

A continuous, periodic function has compact range.

theorem Function.Periodic.isBounded_of_continuous {α : Type u} [PseudoMetricSpace α] {f : ℝ → α} {c : ℝ} (hp : Function.Periodic f c) (hc : c ≠ 0) (hf : Continuous f) : Bornology.IsBounded (Set.range f)

A continuous, periodic function is bounded.

instance Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples {a : ℝ} : DiscreteTopology ↥(AddSubgroup.zmultiples a)

This is a special case of NormedSpace.discreteTopology_zmultiples. It exists only to simplify dependencies.

Equations

• ⋯ = ⋯

theorem Int.tendsto_coe_cofinite : Filter.Tendsto Int.cast Filter.cofinite (Filter.cocompact ℝ)

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.zmultiples a).subtype) 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.