isPreconnected_of_isPreconnected_op

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isPreconnected_of_isPreconnected_op

English

If Jᵒᵖ is preconnected, then J is preconnected.

Русский

Если Jᵒᵖ предсвязан, то J тоже предсвязан.

LaTeX

$$$[\\mathrm{IsPreconnected}(J^{\\mathrm{op}})] \\Rightarrow \\mathrm{IsPreconnected}(J)$$$

Lean4

theorem isPreconnected_of_isPreconnected_op [IsPreconnected Jᵒᵖ] : IsPreconnected J :=
  isPreconnected_of_equivalent (opOpEquivalence J)

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

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

Разделы

Аффилиация

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