instEffectivelyEnoughOfIsEquivalence

Mathlib.CategoryTheory.EffectiveEpi.Enough

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instEffectivelyEnoughOfIsEquivalence

English

If F is an equivalence, then F is effectively enough.

Русский

Если F является эквивалентностью, то F является effectively enough.

LaTeX

$$$[\text{IsEquivalence } F] \Rightarrow \operatorname{EffectivelyEnough} F$$$

Lean4

instance [IsEquivalence F] : EffectivelyEnough F where
  presentation X := ⟨equivalenceEffectivePresentation F.asEquivalence X⟩

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

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

Разделы

Аффилиация

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