coe_of_s_get?_rat_eq — Mathlib

English

If v = ↑q for rational q, then the s-structure of of q, mapped to K, equals the s-structure of v.

Русский

Если v = ↑q, то структура s конвергента of q равна структуре s конвергента v после отображения в K.

LaTeX

$$$(v = (q : K)) \\rightarrow (\\mathrm{of}\\, q).s.map (Pair.map (\\uparrow)) = (\\mathrm{of}\\, v).s$$$

Lean4

theorem coe_of_s_get?_rat_eq (v_eq_q : v = (↑q : K)) (n : ℕ) :
    (((of q).s.get? n).map (Pair.map (↑)) : Option <| Pair K) = (of v).s.get? n :=
  by
  simp only [of, IntFractPair.seq1, Stream'.Seq.map_get?, Stream'.Seq.get?_tail]
  simp only [Stream'.Seq.get?]
  rw [← IntFractPair.coe_stream'_rat_eq v_eq_q]
  rcases succ_nth_stream_eq : IntFractPair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
    simp [Stream'.map, Stream'.get, succ_nth_stream_eq]

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