map_op_inv — Mathlib

English

The map of the inverse Finset under opEquiv.toEmbedding equals the inverse of the map of the Finset: s⁻¹.map opEquiv.toEmbedding = (s.map opEquiv.toEmbedding)⁻¹.

Русский

Обображение обратного Finset через внедрение opEquiv.toEmbedding равно обратному отображению Finset: s⁻¹.map … = (s.map …)⁻¹.

LaTeX

$$$ s^{-1}.map\ opEquiv.toEmbedding = (s.map\ opEquiv.toEmbedding)^{-1} $$$

Lean4

@[to_additive]
theorem map_op_inv (s : Finset α) : s⁻¹.map opEquiv.toEmbedding = (s.map opEquiv.toEmbedding)⁻¹ := by
  simp [map_eq_image, image_op_inv]

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