symm_image_image_of_subset_source

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.symm_image_image_of_subset_source

English

The image of e.symm on e''s subset equals the original subset: SymmImageImageOfSubsetSource.

Русский

Образ e.symm на подмножество образа равен исходному подмножеству.

LaTeX

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

Lean4

theorem symm_image_image_of_subset_source {s : Set α} (h : s ⊆ e.source) : e.symm '' (e '' s) = s :=
  (e.leftInvOn.mono h).image_image

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru