terminates_of_liftRel — Mathlib

English

LiftRel preserves termination: if s is LiftRel-related to t, then s terminates iff t terminates.

Русский

LiftRel сохраняет завершение: если s связано с t через LiftRel, то s завершается тогда и только тогда, когда завершается t.

LaTeX

$$$\\forall {R:\\alpha\\to\\alpha\\to\\mathrm{Prop}}\\ {s t},\\ \\mathrm{LiftRel}\\,R\\ s\\ t \\Rightarrow (\\mathrm{Terminates}\\ s \\leftrightarrow \\mathrm{Terminates}\\ t)$$$

Lean4

theorem terminates_of_liftRel {R : α → β → Prop} {s t} : LiftRel R s t → (Terminates s ↔ Terminates t)
  | ⟨l, r⟩ =>
    ⟨fun ⟨⟨_, as⟩⟩ =>
      let ⟨b, bt, _⟩ := l as
      ⟨⟨b, bt⟩⟩,
      fun ⟨⟨_, bt⟩⟩ =>
      let ⟨a, as, _⟩ := r bt
      ⟨⟨a, as⟩⟩⟩

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