piCongrLeft_comp_frestrictLe — Mathlib

English

A similar conjugation with frestrictLe and restrictLe yields restrictLe.

Русский

Аналогично, сопряжение с frestrictLe и restrictLe даёт restrictLe.

LaTeX

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

Lean4

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

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