isStronglyConnected

Mathlib.Combinatorics.Quiver.ConnectedComponent

URI: https://scilib.ai/kg/mathlib#Quiver.IsSStronglyConnected.isStronglyConnected

English

If a quiver is IsSStronglyConnected, then it is IsStronglyConnected.

Русский

Если квир является IsSStronglyConnected, то он является IsStronglyConnected.

LaTeX

$$$ IsSStronglyConnected(V) \\rightarrow IsStronglyConnected(V) $$$

Lean4

theorem isStronglyConnected (h : IsSStronglyConnected V) : IsStronglyConnected V := by intro i j;
  obtain ⟨p, _⟩ := h i j; exact ⟨p⟩

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

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

Разделы

Аффилиация

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