Matroid.Graph.Lattice

source

theorem Graph.WithTop.eq_top_or_eq_some {α : Type u_5} (a' : WithTop α) :

a' = ⊤ ∨ ∃ (a : α), a' = ↑a

source

noncomputable def Graph.WithTop.sInter {α : Type u_1} {β : Type u_2} (s : Set (WithTop (Graph α β))) :

WithTop (Graph α β)

Equations

Graph.WithTop.sInter s = if hs : ∃ (G : Graph α β), ↑G ∈ s then ↑(Graph.sInter (WithTop.some ⁻¹' s) hs) else ⊤

Instances For

source

noncomputable instance Graph.WithTop.instCompleteSemilatticeInfWithTop_matroid {α : Type u_1} {β : Type u_2} :

CompleteSemilatticeInf (WithTop (Graph α β))

Equations

Graph.WithTop.instCompleteSemilatticeInfWithTop_matroid = { toPartialOrder := WithTop.partialOrder, sInf := Graph.WithTop.sInter, sInf_le := ⋯, le_sInf := ⋯ }

source

noncomputable instance Graph.WithTop.instCompleteLatticeWithTop_matroid {α : Type u_1} {β : Type u_2} :

CompleteLattice (WithTop (Graph α β))

Equations

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

source

@[reducible]

def Graph.Subgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) :

Type (max 0 u_1 u_2)

Equations

G.Subgraph = { H : Graph α β // H ≤ G }

Instances For

source

instance Graph.Subgraph.instCoeOut {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CoeOut G.Subgraph (Graph α β)

Equations

Graph.Subgraph.instCoeOut = { coe := fun (H : G.Subgraph) => ↑H }

source

@[simp]

theorem Graph.Subgraph.le {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.Subgraph) :

↑H ≤ G

source

instance Graph.Subgraph.instPartialOrder {α : Type u_1} {β : Type u_2} {G : Graph α β} :

PartialOrder G.Subgraph

Equations

Graph.Subgraph.instPartialOrder = inferInstanceAs (PartialOrder { H : Graph α β // H ≤ G })

source

@[simp]

theorem Graph.Subgraph.mk_le_iff {α : Type u_1} {β : Type u_2} {G H₁ : Graph α β} {hH₁ : H₁ ≤ G} {H : G.Subgraph} :

⟨H₁, hH₁⟩ ≤ H ↔ H₁ ≤ ↑H

source

@[simp]

theorem Graph.Subgraph.le_mk_iff {α : Type u_1} {β : Type u_2} {G H₁ : Graph α β} {hH₁ : H₁ ≤ G} {H : G.Subgraph} :

H ≤ ⟨H₁, hH₁⟩ ↔ ↑H ≤ H₁

source

@[simp]

theorem Graph.Subgraph.compatible {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.Subgraph) :

(↑H₁).Compatible ↑H₂

source

@[simp]

theorem Graph.Subgraph.pairwise_compatible {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (H : ι → G.Subgraph) :

Pairwise (Function.onFun Compatible fun (i : ι) => ↑(H i))

source

@[simp]

theorem Graph.Subgraph.set_pairwise_compatible {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.Subgraph) :

(Subtype.val '' s).Pairwise Compatible

source

instance Graph.Subgraph.instCompleteLattice {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CompleteLattice G.Subgraph

The proof that the subgraphs of a graph G form a completely distributive lattice.

Equations

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

source

@[simp]

theorem Graph.Subgraph.coe_top {α : Type u_1} {β : Type u_2} {G : Graph α β} :

↑⊤ = G

source

@[simp]

theorem Graph.Subgraph.coe_bot {α : Type u_1} {β : Type u_2} {G : Graph α β} :

↑⊥ = ⊥

source

theorem Graph.Subgraph.coe_iInf {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (H : ι → G.Subgraph) :

↑(⨅ (i : ι), H i) = Graph.iInter fun (x : Option ι) => x.elim G fun (x : ι) => ↑(H x)

source

@[simp]

theorem Graph.Subgraph.iInf_of_isEmpty {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} [IsEmpty ι] (H : ι → G.Subgraph) :

↑(⨅ (i : ι), H i) = G

source

@[simp]

theorem Graph.Subgraph.coe_iInf_of_nonempty {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} [Nonempty ι] (H : ι → G.Subgraph) :

↑(⨅ (i : ι), H i) = Graph.iInter fun (i : ι) => ↑(H i)

source

theorem Graph.Subgraph.coe_sInf {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.Subgraph) :

↑(sInf s) = Graph.sInter (insert G (Subtype.val '' s)) ⋯

source

theorem Graph.Subgraph.coe_sInf_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.Subgraph) (hs : s.Nonempty) :

↑(sInf s) = Graph.sInter (Subtype.val '' s) ⋯

source

theorem Graph.Subgraph.coe_sInf_of_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} :

↑(sInf ∅) = G

source

@[simp]

theorem Graph.Subgraph.coe_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (H : ι → G.Subgraph) :

↑(⨆ (i : ι), H i) = Graph.iUnion (fun (i : ι) => ↑(H i)) ⋯

source

@[simp]

theorem Graph.Subgraph.coe_sSup {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.Subgraph) :

↑(sSup s) = Graph.sUnion (Subtype.val '' s) ⋯

source

@[simp]

theorem Graph.Subgraph.coe_sup {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.Subgraph) :

↑(H₁ ⊔ H₂) = ↑H₁ ∪ ↑H₂

source

@[simp]

theorem Graph.Subgraph.coe_sup_eq_union {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.Subgraph) :

↑(H₁ ⊔ H₂) = ↑H₁ ∪ ↑H₂

source

@[simp]

theorem Graph.Subgraph.coe_inf {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.Subgraph) :

↑(H₁ ⊓ H₂) = ↑H₁ ∩ ↑H₂

source

@[simp]

theorem Graph.Subgraph.range_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} (f : ι' → ι) (H : ι → G.Subgraph) :

⨆ (i : ↑(Set.range f)), H ↑i = ⨆ (i : ι'), H (f i)

source

@[simp]

theorem Graph.Subgraph.range_iInf {α : Type u_1} {β : Type u_2} {ι : Type u_3} {ι' : Type u_4} {G : Graph α β} (f : ι' → ι) (H : ι → G.Subgraph) :

⨅ (i : ↑(Set.range f)), H ↑i = ⨅ (i : ι'), H (f i)

source

theorem Graph.Subgraph.disjoint_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.Subgraph) :

Disjoint H₁ H₂ ↔ (↑H₁).StronglyDisjoint ↑H₂

source

def Graph.Subgraph.of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (H' : H.Subgraph) (hle : H ≤ G) :

G.Subgraph

Equations

H'.of_le hle = ⟨↑H', ⋯⟩

Instances For

source

@[simp]

theorem Graph.Subgraph.coe_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (H' : H.Subgraph) (hle : H ≤ G) :

↑(H'.of_le hle) = ↑H'

source

def Graph.Subgraph.minAx {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CompletelyDistribLattice.MinimalAxioms G.Subgraph

The proof that the subgraphs of a graph G form a completely distributive lattice.

Equations

Graph.Subgraph.minAx = { toCompleteLattice := Graph.Subgraph.instCompleteLattice, iInf_iSup_eq := ⋯ }

Instances For

source

instance Graph.Subgraph.instCompletelyDistribLattice {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CompletelyDistribLattice G.Subgraph

The subgraphs of a graph G form a completely distributive lattice.

Equations

Graph.Subgraph.instCompletelyDistribLattice = CompletelyDistribLattice.ofMinimalAxioms Graph.Subgraph.minAx

source

@[reducible]

def Graph.ClosedSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) :

Type (max 0 u_2 u_1)

Equations

G.ClosedSubgraph = { H : Graph α β // H.IsClosedSubgraph G }

Instances For

source

instance Graph.ClosedSubgraph.instPartialOrder {α : Type u_1} {β : Type u_2} {G : Graph α β} :

PartialOrder G.ClosedSubgraph

Equations

Graph.ClosedSubgraph.instPartialOrder = inferInstanceAs (PartialOrder { H : Graph α β // H.IsClosedSubgraph G })

source

def Graph.ClosedSubgraph.toSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} :

G.ClosedSubgraph ↪o G.Subgraph

The order embedding from closed subgraphs to subgraphs

Equations

Graph.ClosedSubgraph.toSubgraph = Subtype.orderEmbedding ⋯

Instances For

source

@[simp]

theorem Graph.ClosedSubgraph.toSubgraph_val_eq_val {α : Type u_1} {β : Type u_2} {G : Graph α β} :

(fun (x : G.ClosedSubgraph) => ↑(toSubgraph x)) = Subtype.val

source

@[simp]

theorem Graph.ClosedSubgraph.coe_toSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) :

↑(toSubgraph H) = ↑H

source

@[simp]

theorem Graph.ClosedSubgraph.coe_comp_toSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} :

Subtype.val ∘ ⇑toSubgraph = Subtype.val

source

instance Graph.ClosedSubgraph.instCoeOut {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CoeOut G.ClosedSubgraph (Graph α β)

Equations

Graph.ClosedSubgraph.instCoeOut = { coe := fun (H : G.ClosedSubgraph) => ↑H }

source

@[simp]

theorem Graph.ClosedSubgraph.mk_le_iff {α : Type u_1} {β : Type u_2} {G H₁ : Graph α β} {hH₁ : H₁.IsClosedSubgraph G} {H : G.ClosedSubgraph} :

⟨H₁, hH₁⟩ ≤ H ↔ H₁ ≤ ↑H

source

@[simp]

theorem Graph.ClosedSubgraph.le_mk_iff {α : Type u_1} {β : Type u_2} {G H₁ : Graph α β} {hH₁ : H₁.IsClosedSubgraph G} {H : G.ClosedSubgraph} :

H ≤ ⟨H₁, hH₁⟩ ↔ ↑H ≤ H₁

source

instance Graph.ClosedSubgraph.instLattice {α : Type u_1} {β : Type u_2} {G : Graph α β} :

Lattice G.ClosedSubgraph

Equations

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

source

theorem Graph.ClosedSubgraph.coe_le_coe {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₀ H : G.ClosedSubgraph} :

↑H₀ ≤ ↑H ↔ H₀ ≤ H

source

theorem Graph.ClosedSubgraph.coe_lt_coe {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₀ H : G.ClosedSubgraph} :

↑H₀ < ↑H ↔ H₀ < H

source

theorem Graph.ClosedSubgraph.toSubgraph_le_toSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} :

toSubgraph H₁ ≤ toSubgraph H₂ ↔ H₁ ≤ H₂

source

theorem Graph.ClosedSubgraph.toSubgraph_lt_toSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} :

toSubgraph H₁ < toSubgraph H₂ ↔ H₁ < H₂

source

@[simp]

theorem Graph.ClosedSubgraph.coe_sup {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

↑(H₁ ⊔ H₂) = ↑H₁ ∪ ↑H₂

source

@[simp]

theorem Graph.ClosedSubgraph.coe_inf {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

↑(H₁ ⊓ H₂) = ↑H₁ ∩ ↑H₂

source

@[simp]

theorem Graph.ClosedSubgraph.pairwise_compatible {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (H : ι → G.ClosedSubgraph) :

Pairwise (Function.onFun Compatible fun (i : ι) => ↑(H i))

source

@[simp]

theorem Graph.ClosedSubgraph.set_pairwise_compatible {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

(Subtype.val '' s).Pairwise Compatible

source

@[simp]

theorem Graph.ClosedSubgraph.sup_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

(↑(H₁ ⊔ H₂)).vertexSet = (↑H₁).vertexSet ∪ (↑H₂).vertexSet

source

@[simp]

theorem Graph.ClosedSubgraph.sup_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

(↑(H₁ ⊔ H₂)).edgeSet = (↑H₁).edgeSet ∪ (↑H₂).edgeSet

source

@[simp]

theorem Graph.ClosedSubgraph.inf_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

(↑(H₁ ⊓ H₂)).vertexSet = (↑H₁).vertexSet ∩ (↑H₂).vertexSet

source

instance Graph.ClosedSubgraph.instCompleteBooleanAlgebra {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CompleteBooleanAlgebra G.ClosedSubgraph

Equations

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

source

@[simp]

theorem Graph.ClosedSubgraph.coe_top {α : Type u_1} {β : Type u_2} {G : Graph α β} :

↑⊤ = G

source

@[simp]

theorem Graph.ClosedSubgraph.coe_bot {α : Type u_1} {β : Type u_2} {G : Graph α β} :

↑⊥ = ⊥

source

@[simp]

theorem Graph.ClosedSubgraph.toSubgraph_sSup {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

toSubgraph (sSup s) = ⨆ (H : ↑s), toSubgraph ↑H

source

@[simp]

theorem Graph.ClosedSubgraph.coe_sSup {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

↑(sSup s) = Graph.sUnion (Subtype.val '' s) ⋯

source

@[simp]

theorem Graph.ClosedSubgraph.toSubgraph_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (f : ι → G.ClosedSubgraph) :

toSubgraph (⨆ (i : ι), f i) = ⨆ (i : ι), toSubgraph (f i)

source

@[simp]

theorem Graph.ClosedSubgraph.coe_iSup {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (f : ι → G.ClosedSubgraph) (hf : Pairwise (Function.onFun Compatible fun (i : ι) => ↑(f i))) :

↑(⨆ (i : ι), f i) = Graph.iUnion (fun (i : ι) => ↑(f i)) hf

source

@[simp]

theorem Graph.ClosedSubgraph.vertexSet_sSup {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

(↑(sSup s)).vertexSet = ⋃ a ∈ s, (↑a).vertexSet

source

@[simp]

theorem Graph.ClosedSubgraph.edgeSet_sSup {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

(↑(sSup s)).edgeSet = ⋃ a ∈ s, (↑a).edgeSet

source

@[simp]

theorem Graph.ClosedSubgraph.toSubgraph_iInf {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} (f : ι → G.ClosedSubgraph) :

toSubgraph (⨅ (i : ι), f i) = ⨅ (i : ι), toSubgraph (f i)

source

@[simp]

theorem Graph.ClosedSubgraph.coe_iInf_of_nonempty {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} [Nonempty ι] (f : ι → G.ClosedSubgraph) :

↑(⨅ (i : ι), f i) = Graph.iInter fun (i : ι) => ↑(f i)

source

@[simp]

theorem Graph.ClosedSubgraph.coe_iInf_of_empty {α : Type u_1} {β : Type u_2} {ι : Type u_3} {G : Graph α β} [IsEmpty ι] (f : ι → G.ClosedSubgraph) :

↑(⨅ (i : ι), f i) = G

source

@[simp]

theorem Graph.ClosedSubgraph.toSubgraph_sInf {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

toSubgraph (sInf s) = sInf (⇑toSubgraph '' s)

source

@[simp]

theorem Graph.ClosedSubgraph.coe_sInf {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

↑(sInf s) = Graph.sInter (insert G (Subtype.val '' s)) ⋯

source

@[simp]

theorem Graph.ClosedSubgraph.coe_sInf_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {s : Set G.ClosedSubgraph} (hs : s.Nonempty) :

↑(sInf s) = Graph.sInter (Subtype.val '' s) ⋯

source

@[simp]

theorem Graph.ClosedSubgraph.coe_sInf_of_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} :

↑(sInf ∅) = G

source

theorem Graph.ClosedSubgraph.vertexSet_sInf_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} (s : Set G.ClosedSubgraph) :

(↑(sInf s)).vertexSet = G.vertexSet ∩ ⋂ a ∈ s, (↑a).vertexSet

source

@[simp]

theorem Graph.ClosedSubgraph.vertexSet_sInf_comm_of_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {s : Set G.ClosedSubgraph} (hs : s.Nonempty) :

(↑(sInf s)).vertexSet = ⋂ a ∈ s, (↑a).vertexSet

source

instance Graph.ClosedSubgraph.instCompleteAtomicBooleanAlgebra {α : Type u_1} {β : Type u_2} {G : Graph α β} :

CompleteAtomicBooleanAlgebra G.ClosedSubgraph

Equations

Graph.ClosedSubgraph.instCompleteAtomicBooleanAlgebra = { toCompleteBooleanAlgebra := Graph.ClosedSubgraph.instCompleteBooleanAlgebra, iInf_iSup_eq := ⋯ }

source

theorem Graph.ClosedSubgraph.compatible {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

(↑H₁).Compatible ↑H₂

source

@[simp]

theorem Graph.ClosedSubgraph.coe_eq_induce {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) :

G[(↑H).vertexSet] = ↑H

source

theorem Graph.ClosedSubgraph.ext_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} (h : (↑H₁).vertexSet = (↑H₂).vertexSet) :

H₁ = H₂

source

theorem Graph.ClosedSubgraph.vertexSet_inj {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} :

H₁ = H₂ ↔ (↑H₁).vertexSet = (↑H₂).vertexSet

source

theorem Graph.ClosedSubgraph.vertexSet_injective {α : Type u_1} {β : Type u_2} {G : Graph α β} :

Function.Injective fun (x : G.ClosedSubgraph) => (↑x).vertexSet

source

theorem Graph.ClosedSubgraph.vertexSet_strictMono {α : Type u_1} {β : Type u_2} (G : Graph α β) :

StrictMono fun (x : G.ClosedSubgraph) => (↑x).vertexSet

source

theorem Graph.ClosedSubgraph.disjoint_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

Disjoint H₁ H₂ ↔ (↑H₁).StronglyDisjoint ↑H₂

source

theorem Graph.ClosedSubgraph.disjoint_iff_vertexSet_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} :

Disjoint H₁ H₂ ↔ Disjoint (↑H₁).vertexSet (↑H₂).vertexSet

source

theorem Graph.ClosedSubgraph.disjoint_iff_val_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.ClosedSubgraph) :

Disjoint H₁ H₂ ↔ Disjoint ↑H₁ ↑H₂

source

@[simp]

theorem Graph.ClosedSubgraph.eq_ambient_of_subset_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {H : G.ClosedSubgraph} (h : G.vertexSet ⊆ (↑H).vertexSet) :

H = ⊤

source

theorem Graph.ClosedSubgraph.le_iff_vertexSet_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} :

H₁ ≤ H₂ ↔ (↑H₁).vertexSet ⊆ (↑H₂).vertexSet

source

theorem Graph.ClosedSubgraph.lt_iff_vertexSet_ssubset {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.ClosedSubgraph} :

H₁ < H₂ ↔ (↑H₁).vertexSet ⊂ (↑H₂).vertexSet

source

@[simp]

theorem Graph.ClosedSubgraph.compl_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) :

(↑Hᶜ).vertexSet = G.vertexSet \ (↑H).vertexSet

source

@[simp]

theorem Graph.ClosedSubgraph.compl_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) :

(↑Hᶜ).edgeSet = G.edgeSet \ (↑H).edgeSet

source

@[simp]

theorem Graph.ClosedSubgraph.compl_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (H : G.ClosedSubgraph) :

(↑Hᶜ).IsLink e x y ↔ G.IsLink e x y ∧ e ∉ (↑H).edgeSet

source

theorem Graph.ClosedSubgraph.compl_eq_of_stronglyDisjoint_union {α : Type u_1} {β : Type u_2} {H₁ H₂ : Graph α β} (hdisj : H₁.StronglyDisjoint H₂) :

⟨H₁, ⋯⟩ᶜ = ⟨H₂, ⋯⟩

source

theorem Graph.ClosedSubgraph.isAtom_iff_isCompOf {α : Type u_1} {β : Type u_2} {G : Graph α β} (H : G.ClosedSubgraph) :

IsAtom H ↔ (↑H).IsCompOf G

source

theorem Graph.IsClosedSubgraph.eq_induce {α : Type u_1} {β : Type u_2} {G H₁ : Graph α β} (hcl : H₁.IsClosedSubgraph G) :

H₁ = G[H₁.vertexSet]

source

theorem Graph.IsClosedSubgraph.vertexSet_inj {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hcl₁ : H₁.IsClosedSubgraph G) (hcl₂ : H₂.IsClosedSubgraph G) :

H₁ = H₂ ↔ H₁.vertexSet = H₂.vertexSet

source

theorem Graph.IsClosedSubgraph.eq_ambient_of_subset_vertexSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hcl : H.IsClosedSubgraph G) (h : G.vertexSet ⊆ H.vertexSet) :

H = G

source

theorem Graph.IsClosedSubgraph.le_iff_vertexSet_subset {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hcl₁ : H₁.IsClosedSubgraph G) (hcl₂ : H₂.IsClosedSubgraph G) :

H₁ ≤ H₂ ↔ H₁.vertexSet ⊆ H₂.vertexSet

source

theorem Graph.IsClosedSubgraph.lt_iff_vertexSet_ssubset {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hcl₁ : H₁.IsClosedSubgraph G) (hcl₂ : H₂.IsClosedSubgraph G) :

H₁ < H₂ ↔ H₁.vertexSet ⊂ H₂.vertexSet

source

theorem Graph.IsCompOf.stronglyDisjoint_of_ne {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} (hco₁ : H₁.IsCompOf G) (hco₂ : H₂.IsCompOf G) (hne : H₁ ≠ H₂) :

H₁.StronglyDisjoint H₂

Distinct components are vertex-disjoint.

source

theorem Graph.IsCompOf.eq_of_mem_mem {α : Type u_1} {β : Type u_2} {x : α} {G H₁ H₂ : Graph α β} (hH₁ : H₁.IsCompOf G) (hH₂ : H₂.IsCompOf G) (hx₁ : x ∈ H₁.vertexSet) (hx₂ : x ∈ H₂.vertexSet) :

H₁ = H₂