piCongrLeft_comp_restrict — Mathlib

English

Restriction commutes with piCongrLeft after transporting along an equivalence with sets: the two compositions are equal.

Русский

Ограничение и piCongrLeft совместимы через эквивалентность: две композиции равны.

LaTeX

$$$ (s.equivToSet\\.piCongrLeft (\\lambda i, \\pi i)) \\circ s.toSet.restrict = s.restrict. $$$

Lean4

theorem _root_.Set.piCongrLeft_comp_restrict :
    (s.equivToSet.symm.piCongrLeft (fun i : s.toSet ↦ π i)) ∘ s.toSet.restrict = s.restrict :=
  rfl

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