lift_eq_iff_equiv — Mathlib

English

LiftRel (· = ·) c1 c2 ↔ c1 ~ c2.

Русский

LiftRel (· = ·) c1 c2 эквивалентно c1 ~ c2.

LaTeX

$$$\operatorname{LiftRel}(\cdot = \cdot)\ c_1\ c_2 \ \leftrightarrow \ c_1 \sim c_2$$$

Lean4

theorem lift_eq_iff_equiv (c₁ c₂ : Computation α) : LiftRel (· = ·) c₁ c₂ ↔ c₁ ~ c₂ :=
  ⟨fun ⟨h1, h2⟩ a =>
    ⟨fun a1 => by let ⟨b, b2, ab⟩ := h1 a1; rwa [ab], fun a2 => by let ⟨b, b1, ab⟩ := h2 a2; rwa [← ab]⟩, fun e =>
    ⟨fun {a} a1 => ⟨a, (e _).1 a1, rfl⟩, fun {a} a2 => ⟨a, (e _).2 a2, rfl⟩⟩⟩

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