Topological properties of ℝ

instance instNoncompactSpaceRealToTopologicalSpaceToUniformSpacePseudoMetricSpace : NoncompactSpace ℝ

Equations

• instNoncompactSpaceRealToTopologicalSpaceToUniformSpacePseudoMetricSpace = instNoncompactSpaceRealToTopologicalSpaceToUniformSpacePseudoMetricSpace.proof_1

theorem Real.uniformContinuous_add : UniformContinuous fun p => p.fst + p.snd

theorem Real.uniformContinuous_neg : UniformContinuous Neg.neg

instance instContinuousStarRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingRealInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingReal : ContinuousStar ℝ

Equations

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

instance instUniformAddGroupRealToUniformSpacePseudoMetricSpaceInstAddGroupReal : UniformAddGroup ℝ

Equations

• instUniformAddGroupRealToUniformSpacePseudoMetricSpaceInstAddGroupReal = instUniformAddGroupRealToUniformSpacePseudoMetricSpaceInstAddGroupReal.proof_1

instance instTopologicalAddGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstAddGroupReal : TopologicalAddGroup ℝ

Equations

• instTopologicalAddGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstAddGroupReal = instTopologicalAddGroupRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstAddGroupReal.proof_1

instance instTopologicalRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceToNonUnitalNonAssocRingToNonAssocRingInstRingReal : TopologicalRing ℝ

Equations

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

instance instTopologicalDivisionRingRealInstDivisionRingRealToTopologicalSpaceToUniformSpacePseudoMetricSpace : TopologicalDivisionRing ℝ

Equations

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

instance instProperSpaceRealPseudoMetricSpace : ProperSpace ℝ

Equations

• instProperSpaceRealPseudoMetricSpace = instProperSpaceRealPseudoMetricSpace.proof_1

instance instSecondCountableTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpace : TopologicalSpace.SecondCountableTopology ℝ

Equations

• instSecondCountableTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpace = (_ : TopologicalSpace.SecondCountableTopology ℝ)

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

@[simp]

theorem Real.cocompact_eq : Filter.cocompact ℝ = Filter.atBot ⊔ Filter.atTop

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

theorem Real.uniformContinuous_inv (s : Set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ (x : ℝ), x ∈ s → r ≤ |x|) : UniformContinuous fun p => (↑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 => (↑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 x_1 => x * x_1) x)

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

@[deprecated continuous_mul]

theorem Real.continuous_mul : Continuous fun p => p.fst * p.snd

instance instCompleteSpaceRealToUniformSpacePseudoMetricSpace : CompleteSpace ℝ

Equations

• instCompleteSpaceRealToUniformSpacePseudoMetricSpace = instCompleteSpaceRealToUniformSpacePseudoMetricSpace.proof_1

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

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.