neg_trans — Mathlib

English

If a relation in an order-connected set is not r-related between two successive pairs, then it is not related between the outer pair.

Русский

Если между двумя последовательностями не выполняется отношение r, то не выполняется между их крайними элементами.

LaTeX

$$$\\forall {\\alpha} {r} [IsOrderConnected \\alpha \\ r] \\{a,b,c\\},\\; (\\\\lnot r a b) \\\\land (\\\\lnot r b c) \\\\rightarrow \\\\lnot r a c$$$

Lean4

theorem neg_trans {r : α → α → Prop} [IsOrderConnected α r] {a b c} (h₁ : ¬r a b) (h₂ : ¬r b c) : ¬r a c :=
  mt (IsOrderConnected.conn a b c) <| by simp [h₁, h₂]

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