comap_id

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.comap_id

English

For any substructure S of P, pulling back along the identity map yields S itself.

Русский

Для любой подструктуры S в P операция обратного отображения по тождественному отображению возвращает саму S.

LaTeX

$$$S.\\mathrm{comap}(\\mathrm{Hom.id}\\, L\\ P) = S$$$

Lean4

@[simp]
theorem comap_id (S : L.Substructure P) : S.comap (Hom.id _ _) = S :=
  ext (by simp)

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

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

Разделы

Аффилиация

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