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
@[simp]
theorem Real.cocompact_eq :
Filter.cocompact = Filter.atBot Filter.atTop
theorem Real.mem_closure_iff {s : Set } {x : } :
x closure s ∀ (ε : ), ε > 0y, y s |y - x| < ε
theorem Real.uniformContinuous_inv (s : Set ) {r : } (r0 : 0 < r) (H : ∀ (x : ), x sr |x|) :
UniformContinuous fun p => (p)⁻¹
@[deprecated HasContinuousInv₀.continuousAt_inv₀]
theorem Real.tendsto_inv {r : } (r0 : r 0) :
Filter.Tendsto (fun q => q⁻¹) (nhds r) (nhds r⁻¹)
@[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.1| < r₁ |x.2| < r₂) :
UniformContinuous fun p => (p).1 * (p).2
@[deprecated continuous_mul]
theorem Real.continuous_mul :
Continuous fun p => 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.

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

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.

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