isBipartiteWith_comm — Mathlib

English

There is an equivalence between bipartite descriptions with swapped sides: G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s.

Русский

Существуют эквивалентности между описаниями двудольности при смене сторон: G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s.

LaTeX

$$G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s$$

Lean4

theorem isBipartiteWith_comm : G.IsBipartiteWith s t ↔ G.IsBipartiteWith t s :=
  ⟨IsBipartiteWith.symm, IsBipartiteWith.symm⟩

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