def Graph.copy {α : Type u_1} {β : Type u_2} [CompleteLattice α] {X : Set α} {P : Partition α} {l : β → α → α → Prop} (G : Graph α β) {E : Set β} (hP : G.vertexPartition = P) (hV : G.vertexSet = X) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ l e x y) : Graph α β

Copy creates an identical graph with different definitions for its vertex set and edge set. This is mainly used to create graphs with improved definitional properties.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.copy_vertexSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] {X : Set α} {P : Partition α} {l : β → α → α → Prop} (G : Graph α β) {E : Set β} (hP : G.vertexPartition = P) (hV : G.vertexSet = X) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ l e x y) : (G.copy hP hV hE h_isLink).vertexSet = X

@[simp]

theorem Graph.copy_isLink {α : Type u_1} {β : Type u_2} [CompleteLattice α] {X : Set α} {P : Partition α} {l : β → α → α → Prop} (G : Graph α β) {E : Set β} (hP : G.vertexPartition = P) (hV : G.vertexSet = X) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ l e x y) (a✝ : β) (a✝¹ a✝² : α) : (G.copy hP hV hE h_isLink).IsLink a✝ a✝¹ a✝² = l a✝ a✝¹ a✝²

@[simp]

theorem Graph.copy_edgeSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] {X : Set α} {P : Partition α} {l : β → α → α → Prop} (G : Graph α β) {E : Set β} (hP : G.vertexPartition = P) (hV : G.vertexSet = X) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ l e x y) : (G.copy hP hV hE h_isLink).edgeSet = E

@[simp]

theorem Graph.copy_vertexPartition {α : Type u_1} {β : Type u_2} [CompleteLattice α] {X : Set α} {P : Partition α} {l : β → α → α → Prop} (G : Graph α β) {E : Set β} (hP : G.vertexPartition = P) (hV : G.vertexSet = X) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ l e x y) : (G.copy hP hV hE h_isLink).vertexPartition = P

theorem Graph.copy_eq_self {α : Type u_1} {β : Type u_2} [CompleteLattice α] {X : Set α} {P : Partition α} {l : β → α → α → Prop} (G : Graph α β) {E : Set β} (hP : G.vertexPartition = P) (hV : G.vertexSet = X) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ l e x y) : G.copy hP hV hE h_isLink = G

def Graph.mk_of_symm {α : Type u_1} {β : Type u_2} [CompleteLattice α] (P : Partition α) (l : β → α → α → Prop) [∀ (e : β), IsSymm α (l e)] : Graph α β

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.mk_of_symm_vertexPartition {α : Type u_1} {β : Type u_2} [CompleteLattice α] (P : Partition α) (l : β → α → α → Prop) [∀ (e : β), IsSymm α (l e)] : (mk_of_symm P l).vertexPartition = P

@[simp]

theorem Graph.mk_of_symm_edgeSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] (P : Partition α) (l : β → α → α → Prop) [∀ (e : β), IsSymm α (l e)] : (mk_of_symm P l).edgeSet = {e : β | ∃ (x : α) (y : α), (fun (e : β) (x y : α) => have l' := Relation.restrict (l e) P.parts; (∀ ⦃a b c d : α⦄, l' a b → l' c d → a = c ∨ a = d) ∧ l' x y) e x y}

@[simp]

theorem Graph.mk_of_symm_vertexSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] (P : Partition α) (l : β → α → α → Prop) [∀ (e : β), IsSymm α (l e)] : (mk_of_symm P l).vertexSet = P.parts

@[simp]

theorem Graph.mk_of_symm_isLink {α : Type u_1} {β : Type u_2} [CompleteLattice α] (P : Partition α) (l : β → α → α → Prop) [∀ (e : β), IsSymm α (l e)] (e : β) (x y : α) : (mk_of_symm P l).IsLink e x y = have l' := Relation.restrict (l e) P.parts; (∀ ⦃a b c d : α⦄, l' a b → l' c d → a = c ∨ a = d) ∧ l' x y

theorem Graph.IsLink.of_mk_of_symm {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} {P : Partition α} {l : β → α → α → Prop} [∀ (e : β), IsSymm α (l e)] (h : (mk_of_symm P l).IsLink e x y) : l e x y

theorem Graph.mk_of_symm_eq_self {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G : Graph α β) : mk_of_symm G.vertexPartition G.IsLink = G

def Graph.mk' {α : Type u_1} {β : Type u_2} [CompleteLattice α] (V : Partition α) (l : β → α → α → Prop) : Graph α β

Equations

• Graph.mk' V l = Graph.mk_of_symm V fun (e : β) => Relation.SymmClosure (l e)

@[simp]

theorem Graph.mk'_isLink {α : Type u_1} {β : Type u_2} [CompleteLattice α] (V : Partition α) (l : β → α → α → Prop) (e : β) (x y : α) : (mk' V l).IsLink e x y = ((∀ ⦃a b c d : α⦄, Relation.restrict (Relation.SymmClosure (l e)) V.parts a b → Relation.restrict (Relation.SymmClosure (l e)) V.parts c d → a = c ∨ a = d) ∧ Relation.restrict (Relation.SymmClosure (l e)) V.parts x y)

@[simp]

theorem Graph.mk'_vertexPartition {α : Type u_1} {β : Type u_2} [CompleteLattice α] (V : Partition α) (l : β → α → α → Prop) : (mk' V l).vertexPartition = V

@[simp]

theorem Graph.mk'_vertexSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] (V : Partition α) (l : β → α → α → Prop) : (mk' V l).vertexSet = V.parts

@[simp]

theorem Graph.mk'_edgeSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] (V : Partition α) (l : β → α → α → Prop) : (mk' V l).edgeSet = {e : β | (∀ ⦃a b c d : α⦄, Relation.restrict (Relation.SymmClosure (l e)) V.parts a b → Relation.restrict (Relation.SymmClosure (l e)) V.parts c d → a = c ∨ a = d) ∧ ∃ (x : α) (x_1 : α), Relation.restrict (Relation.SymmClosure (l e)) V.parts x x_1}

def Graph.noEdge {α : Type u_1} [CompleteLattice α] (P : Partition α) (β : Type u_3) : Graph α β

The graph with vertex set V and no edges

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.noEdge_vertexSet {α : Type u_1} [CompleteLattice α] (P : Partition α) (β : Type u_3) : (Graph.noEdge P β).vertexSet = P.parts

@[simp]

theorem Graph.noEdge_isLink {α : Type u_1} [CompleteLattice α] (P : Partition α) (β : Type u_3) (x✝ : β) (x✝¹ x✝² : α) : (Graph.noEdge P β).IsLink x✝ x✝¹ x✝² = False

@[simp]

theorem Graph.noEdge_edgeSet {α : Type u_1} [CompleteLattice α] (P : Partition α) (β : Type u_3) : (Graph.noEdge P β).edgeSet = ∅

@[simp]

theorem Graph.noEdge_vertexPartition {α : Type u_1} [CompleteLattice α] (P : Partition α) (β : Type u_3) : (Graph.noEdge P β).vertexPartition = P

theorem Graph.eq_empty_or_vertexSet_nonempty {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G : Graph α β) : G = Graph.noEdge ⊥ β ∨ G.vertexSet.Nonempty

@[simp]

theorem Graph.noEdge_le_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} {P : Partition α} : Graph.noEdge P β ≤ G ↔ P.parts ⊆ G.vertexSet

@[simp]

theorem Graph.noEdge_not_inc {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {e : β} {P : Partition α} : ¬(Graph.noEdge P β).Inc e x

@[simp]

theorem Graph.noEdge_not_isLoopAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {e : β} {P : Partition α} : ¬(Graph.noEdge P β).IsLoopAt e x

@[simp]

theorem Graph.noEdge_not_isNonloopAt {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x : α} {e : β} {P : Partition α} : ¬(Graph.noEdge P β).IsNonloopAt e x

@[simp]

theorem Graph.noEdge_not_adj {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {P : Partition α} : ¬(Graph.noEdge P β).Adj x y

theorem Graph.edgeSet_eq_empty_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} : G.edgeSet = ∅ ↔ G = Graph.noEdge G.vertexPartition β

@[simp]

theorem Graph.le_noEdge_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} {P : Partition α} : G ≤ Graph.noEdge P β ↔ G.vertexSet ⊆ P.parts ∧ G.edgeSet = ∅

instance Graph.instOrderBot {α : Type u_1} {β : Type u_2} [CompleteLattice α] : OrderBot (Graph α β)

Equations

• Graph.instOrderBot = { bot := Graph.noEdge ⊥ β, bot_le := ⋯ }

@[simp]

theorem Graph.bot_vertexSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] : ⊥.vertexSet = ⊥

@[simp]

theorem Graph.bot_edgeSet {α : Type u_1} {β : Type u_2} [CompleteLattice α] : ⊥.edgeSet = ⊥

@[simp]

theorem Graph.bot_isClosedSubgraph {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G : Graph α β) : ⊥.IsClosedSubgraph G

@[simp]

theorem Graph.bot_isInducedSubgraph {α : Type u_1} {β : Type u_2} [CompleteLattice α] (G : Graph α β) : ⊥.IsInducedSubgraph G

@[simp]

theorem Graph.noEdge_empty {α : Type u_1} {β : Type u_2} [CompleteLattice α] : Graph.noEdge ⊥ β = ⊥

@[simp]

theorem Graph.bot_not_isLink {α : Type u_1} {β : Type u_2} [CompleteLattice α] {x y : α} {e : β} : ¬⊥.IsLink e x y

@[simp]

theorem Graph.vertexSet_eq_empty_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} : G.vertexSet = ∅ ↔ G = ⊥

@[simp]

theorem Graph.vertexSet_nonempty_iff {α : Type u_1} {β : Type u_2} [CompleteLattice α] {G : Graph α β} : G.vertexSet.Nonempty ↔ G ≠ ⊥

Complete graphs

def Graph.CompleteGraph (n : ℕ+) : Graph (Set ℕ) (Sym2 ℕ)

The complete graph on n vertices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.CompleteGraph_isLink (n : ℕ+) (e : Sym2 ℕ) (x y : Set ℕ) : (CompleteGraph n).IsLink e x y = ∃ i < ↑n, ∃ j < ↑n, i ≠ j ∧ e = s(i, j) ∧ x = {i} ∧ y = {j}

@[simp]

theorem Graph.CompleteGraph_vertexPartition (n : ℕ+) : (CompleteGraph n).vertexPartition = Partition.discrete (Set.Iio ↑n)

@[simp]

theorem Graph.CompleteGraph_edgeSet (n : ℕ+) : (CompleteGraph n).edgeSet = {s : Sym2 ℕ | (∀ i ∈ s, i < ↑n) ∧ ¬s.IsDiag}

@[simp]

theorem Graph.CompleteGraph_vertexSet (n : ℕ+) : (CompleteGraph n).vertexSet = (Partition.discrete (Set.Iio ↑n)).parts

@[simp]

theorem Graph.CompleteGraph_adj (n : ℕ+) (x y : ℕ) (hx : x < ↑n) (hy : y < ↑n) : (CompleteGraph n).Adj {x} {y} ↔ x ≠ y