equiv — Mathlib

English

If R is an equivalence, then LiftRel R is an equivalence on weak sequences.

Русский

Если R — эквивалентность, то LiftRel R — эквивалентность на слабых последовательностях.

LaTeX

$$$$ (R\text{ is Equivalence}) \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)⟩

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