Generalized definition of bipartite graphs with explicit partitions

[binghe]

Hi,

In fsgraphTheory (under "examples/generic_graphs") the existing definition of "partite" graphs asserts the existence of partitions without explicitly putting them as parameters (NOTE: the existing definition makes sense, because the partitions are not unique, even w.r.t {A; B} = {B; A}. e.g. an isolated vertex can belong to any partition.)

[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

But sometimes this definition is not enough. There are theorems explicitly talking about properties of partitions in the statements (e.g. "G contains a matching of A if and only if ...", where A is one partition of the bipartite graph G, among A and B but chosen arbitrarily).

For this purpose, I added the following "gen_bipartite" concept, which has the partitions explicitly as part of the parameters:

[gen_bipartite_def]
⊢ ∀g A B.
    gen_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

And there's also one alternative definition (just like bipartite_def vs. bipartite_alt):

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

P. S. The code changes are backward compatible to existing user code (i.e. all existing theorems and definitions are still there with the same statements as before.)

Chun

[mn200]

Thanks for this!