SimpleGraph.Partition.isPartition
theorem SimpleGraph.Partition.isPartition :
∀ {V : Type u} {G : SimpleGraph V} (self : G.Partition), Setoid.IsPartition self.parts
The theorem `SimpleGraph.Partition.isPartition` states that for any given type `V` and a simple graph `G` of type `V`, if `self` is a partition of the simple graph `G`, then `self.parts` is a proper partition of `V`. In other words, `self.parts` is a collection of sets with no empty set and each element of type `V` belongs to exactly one set in `self.parts`, ensuring the sets to be pairwise disjoint, satisfying the conditions of `Setoid.IsPartition`.
More concisely: If `self` is a partition of a simple graph `G` of type `V`, then `self.parts` is a proper, pairwise disjoint collection of non-empty sets covering `V`.
|
SimpleGraph.Partition.independent
theorem SimpleGraph.Partition.independent :
∀ {V : Type u} {G : SimpleGraph V} (self : G.Partition), ∀ s ∈ self.parts, IsAntichain G.Adj s
This theorem states that for any partition of a simple graph `G` with vertex set `V`, each element `s` in the partition's `parts` is an antichain with respect to the adjacency relation `Adj` of `G`. In other words, in each subset of the partition, no two distinct vertices are adjacent in the graph. In graph theory, this is also known as the condition that each subset of the partition forms an independent set.
More concisely: For any partition of a simple graph's vertex set, each subset of the partition is an independent set with respect to the graph's adjacency relation.
|