isPreconnected — Mathlib

English

If C is IsFilteredOrEmpty, then C is preconnected.

Русский

Если C является IsFilteredOrEmpty, то C является предварительно связной.

LaTeX

$$$\\mathrm{IsFilteredOrEmpty}(C) \\Rightarrow \\mathrm{IsPreconnected}(C)$$$

Lean4

theorem isPreconnected [IsFilteredOrEmpty C] : IsPreconnected C :=
  zigzag_isPreconnected fun j j' =>
    .trans (.single <| .inl <| .intro <| IsFiltered.leftToMax j j')
      (.single <| .inr <| .intro <| IsFiltered.rightToMax j j')

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