viaEmbedding_apply — Mathlib

English

On the image of α under ι, the extended permutation acts like the original permutation.

Русский

На изображении α под вложением ι расширенная перестановка действует как исходная перестановка.

LaTeX

$$$e.\mathrm{viaEmbedding} s (\iota x) = \iota (e x)$$$

Lean4

theorem viaEmbedding_apply (x : α) : e.viaEmbedding ι (ι x) = ι (e x) :=
  extendDomain_apply_image e (ofInjective ι.1 ι.2) x

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