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