equiv — Mathlib

English

If R is an equivalence on α, then LiftRel R is an equivalence on Computation α.

Русский

Если R является эквивалентностью на α, то LiftRel R является эквивалентностью на Computation α.

LaTeX

$$$\\forall R:\\alpha \\to \\alpha \\to \\mathrm{Prop},\\ \\mathrm{Equivalence}\\,R \\Rightarrow \\mathrm{Equivalence}(\\mathrm{LiftRel}\\,R)$$$

Lean4

theorem equiv (R : α → α → Prop) : Equivalence R → Equivalence (LiftRel R)
  | ⟨refl, symm, trans⟩ => ⟨LiftRel.refl R refl, @LiftRel.symm _ R @symm, @LiftRel.trans _ R @trans⟩

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