transGen_of_succ_of_ne — Mathlib

English

If for all i in Ico n m, r i (succ i) and for all i in Ico m n, r (succ i) i hold, and n ≠ m, then there is a TransGen from n to m.

Русский

Если для всех i в Ico n m верно r i (succ i) и для всех i в Ico m n верно r (succ i) i и n ≠ m, то существует TransGen от n к m.

LaTeX

$$TransGen r n m$$

Lean4

/-- For `n ≠ m`,`(n, m)` is in the transitive closure of a relation `~` if `i ~ succ i` and
  `succ i ~ i` for all `i` between `n` and `m`. -/
theorem transGen_of_succ_of_ne (r : α → α → Prop) {n m : α} (h1 : ∀ i ∈ Ico n m, r i (succ i))
    (h2 : ∀ i ∈ Ico m n, r (succ i) i) (hnm : n ≠ m) : TransGen r n m :=
  (reflTransGen_iff_eq_or_transGen.mp (reflTransGen_of_succ r h1 h2)).resolve_left hnm.symm

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