eqvGen_iff — Mathlib

English

If r is an equivalence, then EqvGen r a b is equivalent to r a b.

Русский

Если r — эквивалентность, то EqvGen r a b эквивалентно r a b.

LaTeX

$$$\\\\operatorname{Equivalence} r \\Rightarrow (\\\\operatorname{EqvGen} r a b \\\\Leftrightarrow r a b)$$$

Lean4

theorem eqvGen_iff (h : Equivalence r) : EqvGen r a b ↔ r a b :=
  Iff.intro
    (by
      intro h
      induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc)
    (EqvGen.rel a b)

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