of_terminates_iff_of_rat_terminates

English

For v with q such that v = ↑q, (of v).Terminates ↔ (of q).Terminates.

Русский

Для v с q таким, что v = ↑q, (of v).Terminates эквивалентно (of q).Terminates.

LaTeX

$$$v = (q : K) \\rightarrow (\\mathrm{of}\\, v).Terminates \\leftrightarrow (\\mathrm{of}\\, q).Terminates$$$

Lean4

theorem of_terminates_iff_of_rat_terminates {v : K} {q : ℚ} (v_eq_q : v = (q : K)) :
    (of v).Terminates ↔ (of q).Terminates := by
  constructor <;> intro h <;> obtain ⟨n, h⟩ := h <;> use n <;>
          simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢ <;>
        cases h' : (of q).s.get? n <;>
      simp only [h'] at h <;>
    trivial

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