liftRel_def — Mathlib

English

LiftRel R ca cb is equivalent to a termination equivalence between ca and cb together with a pointwise R-coupling.

Русский

LiftRel R ca cb эквивалентно равенству завершения между ca и cb и попарной связи по R.

LaTeX

$$$\\mathrm{LiftRel}\\,R\\ ca\\ cb \\ \\leftrightarrow\\ (\\mathrm{Terminates}\\ ca \\leftrightarrow \\mathrm{Terminates}\\ cb) \\land \\forall a\\in ca\\,\\forall b\\in cb\\, R\\ a\\ b$$$

Lean4

theorem liftRel_def {R : α → β → Prop} {ca cb} :
    LiftRel R ca cb ↔ (Terminates ca ↔ Terminates cb) ∧ ∀ {a b}, a ∈ ca → b ∈ cb → R a b :=
  ⟨fun h =>
    ⟨terminates_of_liftRel h, fun {a b} ma mb =>
      by
      let ⟨b', mb', ab⟩ := h.left ma
      rwa [mem_unique mb mb']⟩,
    fun ⟨l, r⟩ =>
    ⟨fun {_} ma =>
      let ⟨⟨b, mb⟩⟩ := l.1 ⟨⟨_, ma⟩⟩
      ⟨b, mb, r ma mb⟩,
      fun {_} mb =>
      let ⟨⟨a, ma⟩⟩ := l.2 ⟨⟨_, mb⟩⟩
      ⟨a, ma, r ma mb⟩⟩⟩

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