preimage_image_univ

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.preimage_image_univ

English

The preimage of the image of the universe is the universe: f^{-1}(f(univ)) = univ.

Русский

Предобраз образа универсума равен универсууму: f^{-1}(f(univ)) = univ.

LaTeX

$$$$ f^{-1}(f(\mathrm{univ})) = \mathrm{univ}. $$$$

Lean4

theorem preimage_image_univ {f : α → β} : f ⁻¹' (f '' univ) = univ :=
  Subset.antisymm (fun _ _ => trivial) (subset_preimage_image f univ)

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

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

Разделы

Аффилиация

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