trans — Mathlib

English

If there is a path from x to y in F and a path from y to z in F, then there is a path from x to z in F (concatenation).

Русский

Если существует путь от x к y в F и путь от y к z в F, то существует путь от x к z в F (соединение путей).

LaTeX

$$JoinedIn F x y → JoinedIn F y z → JoinedIn F x z$$

Lean4

theorem trans (hxy : JoinedIn F x y) (hyz : JoinedIn F y z) : JoinedIn F x z :=
  by
  obtain ⟨hx, hy⟩ := hxy.mem
  obtain ⟨hx, hy⟩ := hyz.mem
  simp_all only [joinedIn_iff_joined]
  exact hxy.trans hyz

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