case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ ‖CauSeq.lim f‖ ≤ a
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
⊢ ‖CauSeq.lim f‖ ≤ a
obtain ⟨N, hN⟩ := (CauSeq.equiv_lim f) _ ha
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ ‖CauSeq.lim f - ↑f N + ↑f N‖ ≤ a
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ ‖CauSeq.lim f‖ ≤ a
rw [←sub_add_cancel f.lim (f N)]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ max ‖CauSeq.lim f - ↑f N‖ ‖↑f N‖ ≤ a
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ ‖CauSeq.lim f - ↑f N + ↑f N‖ ≤ a
refine le_trans (padicNormE.nonarchimedean _ _) ?_
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ max ‖↑f N - CauSeq.lim f‖ ‖↑f N‖ ≤ a
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ max ‖CauSeq.lim f - ↑f N‖ ‖↑f N‖ ≤ a
rw [norm_sub_rev]
no goals
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ max ‖↑f N - CauSeq.lim f‖ ‖↑f N‖ ≤ a
exact max_le (le_of_lt (hN _ le_rfl)) (hf _)