piCongrLeft_comp_restrictLe — Mathlib

English

A conjugation by an index equivalence combined with restrictLe yields frestrictLe.

Русский

Сопряжение по эквивалентности индексов в сочетании с restrictLe даёт frestrictLe.

LaTeX

$$$((\\text{Equiv.IicFinsetSet } a)^{-1}.\\text{piCongrLeft} (\\lambda i: Iic a \\to \\pi i)) \\circ \\mathrm{restrictLe}(a) = \\mathrm{frestrictLe}(a)$$$

Lean4

theorem piCongrLeft_comp_restrictLe {a : α} :
    ((Equiv.IicFinsetSet a).symm.piCongrLeft (fun i : Iic a ↦ π i)) ∘ (restrictLe a) = frestrictLe a :=
  rfl

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