Add definition of r-partite graphs and in particular bipartite graphs

[binghe]

Hi,

This PR adds the definition of r-partite graphs and in particular bipartite graphs, in fsgraphTheory.

A graph is called r-partite if its vertex set admits a partition into r classes such that every edge has its ends in different classes (see, e.g., [1, p.17]). Using partitions and part from pred_setTheory, the following definition can be made to precisely capture the textbook definition:

[partite_def]
⊢ ∀r g v.
    partite r g v ⇔
    v partitions V ∧ CARD v = r ∧ ∀n1 n2. {n1; n2} ∈ E ⇒ part v n1 ≠ part v n2

Then the particularly important concept "bipartite graphs" can be defined as an overload:

Overload bipartite = “partite 2”

The following theorem can be seen as a direct definition of bipartite graphs, where A and B are the two partitions:

[bipartite_def]
⊢ ∀g A B.
    bipartite g {A; B} ⇔
    DISJOINT A B ∧ A ≠ ∅ ∧ B ≠ ∅ ∧ A ∪ B = V ∧
    ∀n1 n2. {n1; n2} ∈ E ⇒ n1 ∈ A ∧ n2 ∈ B ∨ n1 ∈ B ∧ n2 ∈ A

P. S. This small work is mainly for our student projects (on fsgraphTheory) where only bipartite graphs are needed so far. The student may just define bipartite graphs directly while my this extra work can be used to replace the direct definition by the above equivalent theorem.

Chun

[1] Diestel, R.: Graph Theory, 5th Electronic Edition (2016). Springer-Verlag, Berlin (2017).

[binghe]

I also propose the following local overloads to ease the term representations for typical fsgraphs:

Overload V[local] = “nodes (g :fsgraph)”
Overload E[local] = “fsgedges (g :fsgraph)”

This allows theorems having statements as close as possible to textbooks. For example, the following [fsgraph_valid] theorem, represented by the above overloads, may be slightly easier to use than the existing [alledges_valid]:

[fsgraph_valid]
⊢ ∀g n1 n2. {n1; n2} ∈ E ⇒ n1 ∈ V ∧ n2 ∈ V ∧ n1 ≠ n2

[binghe]

The definitions are modified. Instead of saying, e.g., a graph is bipartite with explicit partitions A and B, it's enough to say there exists A B:

[bipartite_def]
⊢ ∀g. bipartite g ⇔
      ∃A B.
        DISJOINT A B ∧ A ≠ ∅ ∧ B ≠ ∅ ∧ A ∪ B = V ∧
        ∀n1 n2. {n1; n2} ∈ E ⇒ n1 ∈ A ∧ n2 ∈ B ∨ n1 ∈ B ∧ n2 ∈ A

[bipartite_alt]
⊢ ∀g. bipartite g ⇔
      ∃A B.
        DISJOINT A B ∧ A ≠ ∅ ∧ B ≠ ∅ ∧ A ∪ B = V ∧
        ∀e. e ∈ E ⇒ ∃n1 n2. e = {n1; n2} ∧ n1 ∈ A ∧ n2 ∈ B

The second theorem [bipartite_alt] is an alternative definition.