image_symm_image_of_subset_target

English

The image of e on s equals s if s is contained in the target and restricted through e.symm.

Русский

Образ e на s равен s, если s содержится в целевом множестве и ограничено через e.symm.

LaTeX

$$$\\forall s:\\ Set\\ \\beta,\\; s \\subseteq e.target \\Rightarrow e''(e.symm '' s) = s$$$

Lean4

theorem image_symm_image_of_subset_target {s : Set β} (h : s ⊆ e.target) : e '' (e.symm '' s) = s :=
  e.symm.symm_image_image_of_subset_source h

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