viaFintypeEmbedding_apply_mem_range

English

If b lies in the range of f, then the value of e.viaFintypeEmbedding f at b is determined via the inverse of f on b.

Русский

Если b принадлежит диапазону f, то значение e.viaFintypeEmbedding f на b задаётся через обратную функцию к f.

LaTeX

$$$e.viaFintypeEmbedding f b = f\big(e\big(f^{-1}(\langle b,h\rangle)\big)\big)$ для некоторого h, где b в диапазоне f$$

Lean4

theorem viaFintypeEmbedding_apply_mem_range {b : β} (h : b ∈ Set.range f) :
    e.viaFintypeEmbedding f b = f (e (f.invOfMemRange ⟨b, h⟩)) :=
  by
  simp only [viaFintypeEmbedding, Function.Embedding.invOfMemRange]
  rw [Equiv.Perm.extendDomain_apply_subtype _ _ h]
  congr

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