English
If x lies in the pathComponentIn F y, then the two path components coincide: pathComponentIn F x = pathComponentIn F y.
Русский
Если x принадлежит pathComponentIn F y, то компоненты пути pathComponentIn F x и pathComponentIn F y совпадают.
LaTeX
$$$$x \in \operatorname{pathComponentIn} F y \Rightarrow \operatorname{pathComponentIn} F x = \operatorname{pathComponentIn} F y.$$$$
Lean4
theorem pathComponentIn_congr (h : x ∈ pathComponentIn F y) : pathComponentIn F x = pathComponentIn F y := by ext;
exact ⟨h.trans, h.symm.trans⟩