piCongrLeft'_symm — Mathlib

English

The left-congruence for a constant fiber is symmetric with respect to inversion of the base equivalence: (piCongrLeft' (fun _ => P) e).symm = piCongrLeft' _ e.symm.

Русский

Левая конгруэнтность для константного основания симметрична относительно обращения базового биекции: (piCongrLeft' (fun _ => P) e).symm = piCongrLeft' _ e.symm.

LaTeX

$$$(\pi\text{-}CongrLeft'(\text{fun }\_=>P)\ e)^{\!-1} = \pi\text{-}CongrLeft'\ _\ e^{-1}.$$$

Lean4

/-- This lemma is impractical to state in the dependent case. -/
@[simp]
theorem piCongrLeft'_symm (P : Sort*) (e : α ≃ β) : (piCongrLeft' (fun _ => P) e).symm = piCongrLeft' _ e.symm := by
  ext; simp [piCongrLeft']

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