transGen_eq_self — Mathlib

English

If r is transitive, then TransGen r equals r as a binary relation.

Русский

Если r транзитивно, то TransGen r равняется r как бинарное отношение.

LaTeX

$$$ \forall {α} {r : α \to α \to \mathrm{Prop}}, \mathrm{Transitive} r \to \mathrm{TransGen} r = r $$$

Lean4

theorem transGen_eq_self (trans : Transitive r) : TransGen r = r :=
  funext fun a ↦
    funext fun b ↦
      propext <|
        ⟨fun h ↦ by
          induction h with
          | single hc => exact hc
          | tail _ hcd hac => exact trans hac hcd,
          TransGen.single⟩

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