pathComponentIn_congr — Mathlib

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⟩

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