finsetCongr_toEmbedding — Mathlib

English

The embedding induced by finset congruence agrees with the embedding map for the original bijection.

Русский

Встроенное отображение, полученное от конгруэнтности Finset, совпадает с отображением вложения для исходной биекции.

LaTeX

$$$e.\\mathrm{finsetCongr}.toEmbedding = (\\mathrm{Finset.mapEmbedding}\, e.toEmbedding).toEmbedding$$$

Lean4

theorem finsetCongr_toEmbedding (e : α ≃ β) :
    e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding :=
  rfl

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