sigma_mk_preimage_image_eq_self

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#sigma_mk_preimage_image_eq_self

English

For a fixed index i, the preimage of the image of s under Sigma.mk i is exactly s.

Русский

Для фиксированного индекса i прообраз образа s под Sigma.mk i равен s.

LaTeX

$$$\Sigma\mathrm{mk}~i^{-1}(\Sigma\mathrm{mk}~i '' s) = s$$$

Lean4

theorem sigma_mk_preimage_image_eq_self : Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s := by simp [image]

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

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

Разделы

Аффилиация

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