reflTransGen_of_succ — Mathlib

English

If i ~ succ i and succ i ~ i for all i in Ico n m, then there is a reflexive-transitive chain from n to m.

Русский

Если i ~ succ i и succ i ~ i для всех i в Ico n m, существует рефлексивно-транзитивная цепь от n к m.

LaTeX

$$ReflTransGen r n m$$

Lean4

/-- `(n, m)` is in the reflexive-transitive closure of `~` if `i ~ succ i` and `succ i ~ i`
  for all `i` between `n` and `m`. -/
theorem reflTransGen_of_succ (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ico n m, r i (succ i))
    (h2 : ∀ i ∈ Ico m n, r (succ i) i) : ReflTransGen r n m :=
  (le_total n m).elim (reflTransGen_of_succ_of_le r h1) <| reflTransGen_of_succ_of_ge r h2

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