preimage_image

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.preimage_image

English

If I is a model with corners, then the preimage of the image of any set s under I is exactly s; i.e., I^{-1}(I(s)) = s.

Русский

Пусть I — модель с углами. Тогда предобраз образа множества s равен самому множеству s: I^{-1}(I(s)) = s.

LaTeX

$$$I^{-1}(I(s)) = s$$$

Lean4

theorem preimage_image (s : Set H) : I ⁻¹' (I '' s) = s :=
  I.injective.preimage_image s

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

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

Разделы

Аффилиация

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