pathComponent_congr — Mathlib

English

If x ∈ pathComponent y, then pathComponent x = pathComponent y.

Русский

Если x принадлежит pathComponent y, то pathComponent x = pathComponent y.

LaTeX

$$x ∈ pathComponent y → pathComponent x = pathComponent y$$

Lean4

theorem pathComponent_congr (h : x ∈ pathComponent y) : pathComponent x = pathComponent y :=
  by
  ext z
  constructor
  · intro h'
    rw [pathComponent_symm]
    exact (h.trans h').symm
  · intro h'
    rw [pathComponent_symm] at h' ⊢
    exact h'.trans h

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