Theorems · Theorem · combinatorics

Finset.restrict_comp_piCongrLeft

∀ {α : Type u} {β : Type v} {π : β → Type u_1} (s : Finset β) (e : α ≃ β),
  s.restrict ∘ ⇑(Equiv.piCongrLeft π e) =
    ⇑(Equiv.piCongrLeft (fun b => π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict

Reindexing and then restricting to a Finset is the same as first restricting to the preimage of this Finset and then reindexing.

Defined in

Mathlib.Data.Finset.Preimage

Cited by

1 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound