isConnected_rightwards_iff_downwards

English

For any g, IsConnected of the rightwards structured arrow equals IsConnected of the downwards one: IsConnected (w.StructuredArrowRightwards g) ↔ IsConnected (w.CostructuredArrowDownwards g).

Русский

Для любого g выполняется эквивалентность связности правого и нижнего структурированных стрел: IsConnected (w.StructuredArrowRightwards g) ⇔ IsConnected (w.CostructuredArrowDownwards g).

LaTeX

$$$\operatorname{IsConnected}\big(w.StructuredArrowRightwards g\big) \iff \operatorname{IsConnected}\big(w.CostructuredArrowDownwards g\big)$$$

Lean4

theorem isConnected_rightwards_iff_downwards :
    IsConnected (w.StructuredArrowRightwards g) ↔ IsConnected (w.CostructuredArrowDownwards g) :=
  isConnected_iff_of_equivalence (w.equivalenceJ g)

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