viaEmbedding_apply_of_notMem — Mathlib

English

If x is outside the image of the embedding, the extended permutation fixes x.

Русский

Если x вне образа вложения, расширенная перестановка фиксирует x.

LaTeX

$$$x \notin \operatorname{range}(\iota) \Rightarrow (e.\mathrm{viaEmbedding } \iota)(x) = x$$$

Lean4

theorem viaEmbedding_apply_of_notMem (x : β) (hx : x ∉ Set.range ι) : e.viaEmbedding ι x = x :=
  extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx

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