zigzag_isPreconnected — Mathlib

English

If for every pair j1, j2 we have Zigzag j1 j2, then J is IsPreconnected.

Русский

Если для любых пар j1, j2 выполняется Zigzag j1 j2, то J является IsPreconnected.

LaTeX

$$$\forall J \,[IsPreconnected J]$ или эквивалентно: $(\forall j_1 j_2: J, Zigzag\ j_1 j_2) \Rightarrow IsPreconnected J$$$

Lean4

theorem zigzag_isPreconnected (h : ∀ j₁ j₂ : J, Zigzag j₁ j₂) : IsPreconnected J :=
  by
  apply IsPreconnected.of_constant_of_preserves_morphisms
  intro α F hF j j'
  specialize h j j'
  induction h with
  | refl => rfl
  | tail _ hj ih =>
    rw [ih]
    rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
    exacts [hF hj, (hF hj).symm]

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