isConstant_congr

Mathlib.CategoryTheory.Sites.ConstantSheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.isConstant_congr

← MathLib Explorer

English

If F is constant and F ≅ G, then G is constant as well.

Русский

Если F константна и F ≅ G, то и G константен.

LaTeX

$$$\\text{isConstant\_congr}: (F \\cong G) \\Rightarrow \\text{IsConstant } J F \\Rightarrow \\text{IsConstant } J G$$$

Lean4

theorem isConstant_congr {F G : Sheaf J D} (i : F ≅ G) [IsConstant J F] : IsConstant J G where
  mem_essImage := essImage.ofIso i F.mem_essImage_of_isConstant

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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