finsetCongr_apply — Mathlib

English

For an equivalence e: α ≃ β and a Finset s of α, the image under the induced Finset congruence equals the map of s under e.

Русский

Для эквивалентности e: α ≃ β и Finset s над α, образ через полученную эквиваленцию Finset равен отображению s под e.

LaTeX

$$$e.\\mathrm{finsetCongr}\\; s = s.\\mathrm{map}\\, e.toEmbedding$$$

Lean4

@[simp]
theorem finsetCongr_apply (e : α ≃ β) (s : Finset α) : e.finsetCongr s = s.map e.toEmbedding :=
  rfl

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