image_symm_apply — Mathlib

English

For an injective f and s, applying the inverse of the image bijection to a point from the image returns the original preimage.

Русский

Для инъективной функции f и множества s отображение обратно возвращает исходное значение при применении обратного отображения к точке образа.

LaTeX

$$$ (\\mathrm{Set.image}\, f\, s\\, H)^{-1} \\langle f x, h \\rangle = \\langle x, H.mem\\_set\\_image.1 h\\rangle $$$

Lean4

@[simp]
protected theorem image_symm_apply {α β} (f : α → β) (s : Set α) (H : Injective f) (x : α) (h : f x ∈ f '' s) :
    (Set.image f s H).symm ⟨f x, h⟩ = ⟨x, H.mem_set_image.1 h⟩ :=
  (Equiv.symm_apply_eq _).2 rfl

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