symm_cast — Mathlib

English

If you cast a path and then take its symmetry, this equals casting the symmetry of the original path with the opposite endpoint equalities. Formally, (γ.cast ha hb).symm = γ.symm.cast hb ha.

Русский

Если привести путь, а затем взять его симметрию, то это равно приведению симметрии исходного пути с противоположными равенствами концов. То есть (γ.cast ha hb).symm = γ.symm.cast hb ha.

LaTeX

$$$((\gamma.cast ha hb).symm) = (\gamma.symm).cast hb ha$$$

Lean4

@[simp]
theorem symm_cast {a₁ a₂ b₁ b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) :
    (γ.cast ha hb).symm = γ.symm.cast hb ha :=
  rfl

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