Documentation

Mathlib.Topology.Instances.Real

Topological properties of ℝ #

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]

Alias of atBot_le_cocompact.

@[deprecated atTop_le_cocompact]

Alias of atTop_le_cocompact.

theorem Real.mem_closure_iff {s : Set } {x : } :
x closure s ε > 0, ys, |y - x| < ε
theorem Real.uniformContinuous_inv (s : Set ) {r : } (r0 : 0 < r) (H : xs, r |x|) :
UniformContinuous fun (p : s) => (↑p)⁻¹
theorem Real.continuous_inv :
Continuous fun (a : { r : // r 0 }) => (↑a)⁻¹
theorem Real.uniformContinuous_mul (s : Set ( × )) {r₁ : } {r₂ : } (H : xs, |x.1| < r₁ |x.2| < r₂) :
UniformContinuous fun (p : s) => (↑p).1 * (↑p).2
theorem closure_of_rat_image_lt {q : } :
closure (Rat.cast '' {x : | q < x}) = {r : | q r}
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.

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.

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.

The subgroup "multiples of a" (zmultiples a) is a discrete subgroup of , i.e. its intersection with compact sets is finite.