denseRange_natCast — Mathlib

English

Second-density statement for Nat.cast in ℤ_p.

Русский

Вторая формулировка плотности образа Nat.cast в ℤ_p.

LaTeX

$$DenseRange Nat.cast$$

Lean4

theorem denseRange_natCast : DenseRange (Nat.cast : ℕ → ℤ_[p]) :=
  by
  intro x
  rw [Metric.mem_closure_range_iff]
  intro ε hε
  obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
  use x.appr n
  rw [dist_eq_norm]
  apply lt_of_le_of_lt _ hn
  rw [norm_le_pow_iff_mem_span_pow]
  apply appr_spec

Похожие утверждения