viaFintypeEmbedding_apply_image — Mathlib

English

On the image of f, the viaFintypeEmbedding acts as e transported along f.

Русский

На образе f через viaFintypeEmbedding перестановка действует как e перенесенная вдоль f.

LaTeX

$$$e.viaFintypeEmbedding f (f a) = f (e a)$$$

Lean4

@[simp]
theorem viaFintypeEmbedding_apply_image (a : α) : e.viaFintypeEmbedding f (f a) = f (e a) :=
  by
  rw [Equiv.Perm.viaFintypeEmbedding]
  convert Equiv.Perm.extendDomain_apply_image e (Function.Embedding.toEquivRange f) a

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