rprod_le_transGen_gameAdd — Mathlib

English

The product relation RProd is included in the transitive closure of GameAdd.

Русский

Отношение RProd входит в транзитивное замыкание GameAdd.

LaTeX

$$$RProd \\leq \\text{TransGen} (\\text{GameAdd})$$$

Lean4

/-- `Prod.RProd` is a subrelation of the transitive closure of `Prod.GameAdd`. -/
theorem rprod_le_transGen_gameAdd : RProd rα rβ ≤ Relation.TransGen (GameAdd rα rβ)
  | _, _, h =>
    h.rec
      (by
        intro _ _ _ _ hα hβ
        exact Relation.TransGen.tail (Relation.TransGen.single <| GameAdd.fst hα) (GameAdd.snd hβ))

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