id

Mathlib.CategoryTheory.Functor.Flat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.RepresentablyCoflat.id

English

If F is RepresentablyCoflat and α: F ≅ G is an isomorphism, then G is RepresentablyCoflat.

Русский

Если F RepresentablyCoflat и есть изоморфизм α: F ≅ G, то G тоже RepresentablyCoflat.

LaTeX

$$$$ [\\mathrm{RepresentablyCoflat}(F)] \\Rightarrow [\\alpha: F \\cong G] \\Rightarrow \\mathrm{RepresentablyCoflat}(G). $$$$

Lean4

theorem id : RepresentablyCoflat (𝟭 C) :=
  inferInstance

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

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

Разделы

Аффилиация

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