preimage_id

Mathlib.CategoryTheory.Subpresheaf.Image

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.preimage_id

English

For any subpresheaf G of F, the preimage of the identity on F is G itself.

Русский

Для любой подпрефеши F верна предобраз единицы: предобраз идентичности на F равен самому G.

LaTeX

$$$ G.\\mathrm{preimage}(\\mathrm{id}_F) = G $$$

Lean4

@[simp]
theorem preimage_id (G : Subpresheaf F) : G.preimage (𝟙 F) = G := by aesop

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

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

Разделы

Аффилиация

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