[GOAL]
α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist a✝ b✝ < ε
⊢ dist (-a✝) (-b✝) < ε
[PROOFSTEP]
rw [dist_comm] at h 
[GOAL]
α : Type u
β : Type v
γ : Type w
ε : ℝ
ε0 : ε > 0
a✝ b✝ : ℝ
h : dist b✝ a✝ < ε
⊢ dist (-a✝) (-b✝) < ε
[PROOFSTEP]
simpa only [Real.dist_eq, neg_sub_neg] using h
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ TopologicalAddGroup ℝ
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
x r : ℝ
⊢ IsCompact (closedBall x r)
[PROOFSTEP]
rw [Real.closedBall_eq_Icc]
[GOAL]
α : Type u
β : Type v
γ : Type w
x r : ℝ
⊢ IsCompact (Icc (x - r) (x + r))
[PROOFSTEP]
apply isCompact_Icc
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ ∀ (u : Set ℝ), u ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b} → IsOpen u
[PROOFSTEP]
simp (config := { contextual := true }) [isOpen_Ioo]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ Ioo ↑q ↑p ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
v : Set ℝ
hav : a ∈ v
hv : IsOpen v
l u : ℝ
hl : l < a
hu : a < u
h : Ioo l u ⊆ v
q : ℚ
hlq : l < ↑q
hqa : ↑q < a
p : ℚ
hap : a < ↑p
hpu : ↑p < u
⊢ ∃ i i_1 i_2, Ioo ↑q ↑p ∈ {Ioo ↑i ↑i_1}
[PROOFSTEP]
exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ cocompact ℝ = atBot ⊔ atTop
[PROOFSTEP]
simp only [← comap_dist_right_atTop_eq_cocompact (0 : ℝ), Real.dist_eq, sub_zero, comap_abs_atTop]
[GOAL]
α : Type u
β : Type v
γ : Type w
s : Set ℝ
x : ℝ
⊢ x ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → ∃ y, y ∈ s ∧ |y - x| < ε
[PROOFSTEP]
simp [mem_closure_iff_nhds_basis nhds_basis_ball, Real.dist_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ CompleteSpace ℝ
[PROOFSTEP]
apply complete_of_cauchySeq_tendsto
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
⊢ ∀ (u : ℕ → ℝ), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
intro u hu
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
let c : CauSeq ℝ abs := ⟨u, Metric.cauchySeq_iff'.1 hu⟩
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
⊢ ∃ a, Tendsto u atTop (𝓝 a)
[PROOFSTEP]
refine' ⟨c.lim, fun s h => _⟩
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
⊢ s ∈ map u atTop
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
⊢ s ∈ map u atTop
[PROOFSTEP]
have := c.equiv_lim ε ε0
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
this : ∃ i, ∀ (j : ℕ), j ≥ i → |↑(c - CauSeq.const abs (CauSeq.lim c)) j| < ε
⊢ s ∈ map u atTop
[PROOFSTEP]
simp only [mem_map, mem_atTop_sets, mem_setOf_eq]
[GOAL]
case a.intro.intro
α : Type u
β : Type v
γ : Type w
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℝ
h : s ∈ 𝓝 (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
this : ∃ i, ∀ (j : ℕ), j ≥ i → |↑(c - CauSeq.const abs (CauSeq.lim c)) j| < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → b ∈ u ⁻¹' s
[PROOFSTEP]
refine' this.imp fun N hN n hn => hε (hN n hn)
[GOAL]
α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (ball x ε)
[PROOFSTEP]
rw [Real.ball_eq_Ioo]
[GOAL]
α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
[PROOFSTEP]
apply totallyBounded_Ioo
[GOAL]
α : Type u
β : Type v
γ : Type w
q : ℚ
x : ℝ
hx : x ∈ {r | ↑q ≤ r}
t : Set ℝ
ht : t ∈ 𝓝 x
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ t
p : ℚ
h₁ : x < ↑p
h₂ : ↑p < x + ε
⊢ ↑p ∈ ball x ε
[PROOFSTEP]
rwa [mem_ball, Real.dist_eq, abs_of_pos (sub_pos.2 h₁), sub_lt_iff_lt_add']
[GOAL]
α : Type u
β : Type v
γ : Type w
s : Set ℝ
⊢ Metric.Bounded s → BddBelow s ∧ BddAbove s
[PROOFSTEP]
intro bdd
[GOAL]
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
⊢ BddBelow s ∧ BddAbove s
[PROOFSTEP]
rcases(bounded_iff_subset_ball 0).1 bdd with
  ⟨r, hr⟩
    -- hr : s ⊆ closed_ball 0 r
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ closedBall 0 r
⊢ BddBelow s ∧ BddAbove s
[PROOFSTEP]
rw [Real.closedBall_eq_Icc] at hr 
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ Icc (0 - r) (0 + r)
⊢ BddBelow s ∧ BddAbove s
[PROOFSTEP]
exact ⟨bddBelow_Icc.mono hr, bddAbove_Icc.mono hr⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (range f)
[PROOFSTEP]
rw [← hp.image_uIcc hc 0]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (f '' [[0, 0 + c]])
[PROOFSTEP]
exact isCompact_uIcc.image hf
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples 0 }
[PROOFSTEP]
rw [AddSubgroup.zmultiples_zero_eq_bot]
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ ⊥ }
[PROOFSTEP]
exact Subsingleton.discreteTopology (α := (⊥ : Submodule ℤ ℝ))
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
[PROOFSTEP]
rw [discreteTopology_iff_open_singleton_zero, isOpen_induced_iff]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ ∃ t, IsOpen t ∧ Subtype.val ⁻¹' t = {0}
[PROOFSTEP]
refine' ⟨ball 0 |a|, isOpen_ball, _⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Subtype.val ⁻¹' ball 0 |a| = {0}
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case inr.h.mk
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
x : ℝ
hx : x ∈ AddSubgroup.zmultiples a
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' ball 0 |a| ↔ { val := x, property := hx } ∈ {0}
[PROOFSTEP]
obtain ⟨k, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx
[GOAL]
case inr.h.mk.intro
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : k • a ∈ AddSubgroup.zmultiples a
⊢ { val := k • a, property := hx } ∈ Subtype.val ⁻¹' ball 0 |a| ↔ { val := k • a, property := hx } ∈ {0}
[PROOFSTEP]
simp [ha, Real.dist_eq, abs_mul, (by norm_cast : |(k : ℝ)| < 1 ↔ |k| < 1)]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
k : ℤ
hx : k • a ∈ AddSubgroup.zmultiples a
⊢ |↑k| < 1 ↔ |k| < 1
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ Tendsto Int.cast cofinite (cocompact ℝ)
[PROOFSTEP]
apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ AddMonoidHom.range (castAddHom ℝ) }
[PROOFSTEP]
rw [range_castAddHom]
[GOAL]
α : Type u
β : Type v
γ : Type w
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples 1 }
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ Tendsto (↑(↑(zmultiplesHom ℝ) a)) cofinite (cocompact ℝ)
[PROOFSTEP]
apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete $ smul_left_injective ℤ ha
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology { x // x ∈ AddMonoidHom.range (↑(zmultiplesHom ℝ) a) }
[PROOFSTEP]
rw [AddSubgroup.range_zmultiplesHom]
[GOAL]
α : Type u
β : Type v
γ : Type w
a : ℝ
ha : a ≠ 0
⊢ DiscreteTopology { x // x ∈ AddSubgroup.zmultiples a }
[PROOFSTEP]
infer_instance
