Topological properties of ℝ

instance instNoncompactSpaceRealToTopologicalSpaceToUniformSpacePseudoMetricSpace : NoncompactSpace ℝ

Equations

• instNoncompactSpaceRealToTopologicalSpaceToUniformSpacePseudoMetricSpace = ⋯

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

theorem Real.uniformContinuous_neg : UniformContinuous Neg.neg

instance instContinuousStarRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRingInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing : ContinuousStar ℝ

Equations

• One or more equations did not get rendered due to their size.

instance instUniformAddGroupRealToUniformSpacePseudoMetricSpaceInstAddGroupReal : UniformAddGroup ℝ

Equations

• instUniformAddGroupRealToUniformSpacePseudoMetricSpaceInstAddGroupReal = ⋯

instance instTopologicalAddGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstAddGroupReal : TopologicalAddGroup ℝ

Equations

• instTopologicalAddGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstAddGroupReal = ⋯

instance instTopologicalRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceToNonUnitalNonAssocRingToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing : TopologicalRing ℝ

Equations

• instTopologicalRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceToNonUnitalNonAssocRingToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing = ⋯

instance instTopologicalDivisionRingRealInstDivisionRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace : TopologicalDivisionRing ℝ

Equations

• instTopologicalDivisionRingRealInstDivisionRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace = ⋯

instance instProperSpaceRealPseudoMetricSpace : ProperSpace ℝ

Equations

• instProperSpaceRealPseudoMetricSpace = ⋯

instance instSecondCountableTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpace : SecondCountableTopology ℝ

Equations

• instSecondCountableTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpace = ⋯

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

@[deprecated HasContinuousInv₀.continuousAt_inv₀]

theorem Real.tendsto_inv {r : ℝ} (r0 : r ≠ 0) : Filter.Tendsto (fun (q : ℝ) => q⁻¹) (nhds r) (nhds r⁻¹)

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

@[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.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

@[deprecated continuous_mul]

theorem Real.continuous_mul : Continuous fun (p : ℝ × ℝ) => p.1 * p.2

instance instCompleteSpaceRealToUniformSpacePseudoMetricSpace : CompleteSpace ℝ

Equations

• instCompleteSpaceRealToUniformSpacePseudoMetricSpace = ⋯

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}

theorem Real.isBounded_iff_bddBelow_bddAbove {s : Set ℝ} : Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

theorem Real.subset_Icc_sInf_sSup_of_isBounded {s : Set ℝ} (h : Bornology.IsBounded s) : s ⊆ Set.Icc (sInf s) (sSup s)

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.

@[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) : IsCompact (Set.range f)

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.instDiscreteTopologySubtypeRealMemAddSubgroupInstAddGroupRealInstMembershipInstSetLikeAddSubgroupZmultiplesInstTopologicalSpaceSubtypeToTopologicalSpaceToUniformSpacePseudoMetricSpace {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.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.