bijOn_symm_image

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Equiv.bijOn_symm_image

English

For an equivalence e: α ≃ β, the inverse map e^{-1} gives a bijection from the image e[s] back to s: BijOn e^{-1} (e[s]) s.

Русский

Для эквивалентности e: α ≃ β обратная карта e^{-1} задаёт биекцию от образа e[s] обратно к s: BijOn e^{-1} (e[s]) s.

LaTeX

$$$\mathrm{BijOn}(e^{-1},\,e''s,\,s)$$$

Lean4

theorem bijOn_symm_image : BijOn e.symm (e '' s) s :=
  e.bijOn_image.symm e.invOn

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

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

Разделы

Аффилиация

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