finsetCongr_trans — Mathlib

English

The composition of finset congruences corresponds to the congruence of the composed equivalence.

Русский

Сочетание конгруэнтности Finset соответствует конгруэнтности составленной эквиваленции.

LaTeX

$$$e.\\mathrm{finsetCongr}.trans e'.\\mathrm{finsetCongr} = (e.\\mathrm{trans} e').\\mathrm{finsetCongr}$$$

Lean4

@[simp]
theorem finsetCongr_trans (e : α ≃ β) (e' : β ≃ γ) : e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr :=
  by
  ext
  simp [-Finset.mem_map, -Equiv.trans_toEmbedding]

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