isSStronglyConnected_of_hom — Mathlib

English

If V is strongly connected and e0: i0 → j0 is a fixed arrow, then V is IsSStronglyConnected.

Русский

Если V является сильно связным и задан данный стрел e0: i0 → j0, тогда V является IsSStronglyConnected.

LaTeX

$$$ (\\text{IsStronglyConnected}(V)) \\rightarrow \\big(\\forall i,j:\\ V, \\exists p:\\text{Path}(i,j), 0 < |p|\\big) $$$

Lean4

theorem isSStronglyConnected_of_hom (h_sc : IsStronglyConnected V) {i₀ j₀ : V} (e₀ : i₀ ⟶ j₀) :
    IsSStronglyConnected V := by
  intro i j
  obtain ⟨p₁⟩ := h_sc i i₀
  obtain ⟨p₂⟩ := h_sc j₀ j
  let p : Path i j := p₁.comp (e₀.toPath.comp p₂)
  have hp_pos : 0 < p.length := by
    simpa [p, Path.length_comp, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
      Nat.succ_pos (p₁.length + p₂.length)
  exact ⟨p, hp_pos⟩

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