viaFintypeEmbedding_apply_notMem_range

English

If b is not in the range of f, then e.viaFintypeEmbedding f b equals b itself.

Русский

Если b не принадлежит диапазону f, тогда e.viaFintypeEmbedding f b равно самому b.

LaTeX

$$$\text{If } b \notin \mathrm{range}(f),\quad e.viaFintypeEmbedding f b = b$$$

Lean4

theorem viaFintypeEmbedding_apply_notMem_range {b : β} (h : b ∉ Set.range f) : e.viaFintypeEmbedding f b = b := by
  rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]

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