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

@[instance_reducible]

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

CompleteSemilatticeInf (WithTop (Graph α β))

Equations

Graph.WithTop.instCompleteSemilatticeInfWithTop_matroid = { toPartialOrder := WithTop.instPartialOrder, sInf := Graph.WithTop.sInter, isGLB_sInf := ⋯ }

source

@[instance_reducible]

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_reducible]

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_reducible]

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

PartialOrder G.Subgraph

Equations

Graph.Subgraph.instPartialOrder = { toPreorder := Subtype.preorder fun (H : Graph α β) => H ≤ G, le_antisymm := ⋯ }

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

theorem Graph.Subgraph.ext {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ H₂ : G.Subgraph} (hV : (↑H₁).vertexSet = (↑H₂).vertexSet) (hE : (↑H₁).edgeSet = (↑H₂).edgeSet) :

H₁ = H₂

source

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

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

source

theorem Graph.IsLink.of_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {H₁ H₂ : G.Subgraph} (hxy : (↑H₁).IsLink e x y) (he : e ∈ (↑H₂).edgeSet) :

(↑H₂).IsLink e x y

source

theorem Graph.IsLink.isLink_iff_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {H₁ H₂ : G.Subgraph} (hxy : (↑H₁).IsLink e x y) :

(↑H₂).IsLink e x y ↔ e ∈ (↑H₂).edgeSet

source

theorem Graph.Inc.of_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {H₁ H₂ : G.Subgraph} (h : (↑H₁).Inc e x) (he : e ∈ (↑H₂).edgeSet) :

(↑H₂).Inc e x

source

theorem Graph.Inc.isInc_iff_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {H₁ H₂ : G.Subgraph} (hx : (↑H₁).Inc e x) :

(↑H₂).Inc e x ↔ e ∈ (↑H₂).edgeSet

source

theorem Graph.Subgraph.incVertexSet_subset_of_le_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} {H₂ : G.Subgraph} (H₁ : G.Subgraph) (hF : F ⊆ (↑H₂).edgeSet) :

V(↑H₁, F) ⊆ V(↑H₂, F)

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_reducible]

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

@[simp]

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

H ≠ ⊥ ↔ (↑H).vertexSet.Nonempty

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_stronglyDisjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (H₁ H₂ : G.Subgraph) :

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

source

@[simp]

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

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

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

theorem 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.

source

@[instance_reducible]

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 ⋯

source

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

G.Subgraph

The minimal subgraph of G that contains the edges in F.

Equations

Graph.Subgraph.ofEdge G F = ⟨G[V(G, F)].restrict F, ⋯⟩

Instances For

source

def Graph.Subgraph.«term_↾↾_» :

Lean.TrailingParserDescr

Equations

Graph.Subgraph.«term_↾↾_» = Lean.ParserDescr.trailingNode `Graph.Subgraph.«term_↾↾_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↾↾ ") (Lean.ParserDescr.cat `term 66))

Instances For

source

@[simp]

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

G[V(G, F)].edgeSet ∩ F = G.edgeSet ∩ F

source

@[simp]

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

(↑(ofEdge G F)).vertexSet = V(G, F)

source

@[simp]

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

(↑(ofEdge G F)).edgeSet = G.edgeSet ∩ F

source

@[simp]

theorem Graph.Subgraph.ofEdge_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (F : Set β) :

(↑(ofEdge G F)).IsLink e x y ↔ e ∈ F ∧ G.IsLink e x y

source

@[instance_reducible]

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

Compl G.Subgraph

The complement of a subgraph of G is the minimal subgraph of G that contains the edges and vertices that are not in the subgraph. See compl_le_iff. This complement is not well behaved in general order theoretically. See inf_compl_eq_bot_iff. However, it is useful for other purposes.

Equations

Graph.Subgraph.instCompl = { compl := fun (H : G.Subgraph) => ⟨G[G.vertexSet \ (↑H).vertexSet ∪ V(G, G.edgeSet \ (↑H).edgeSet)].deleteEdges (↑H).edgeSet, ⋯⟩ }

source

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

(↑Hᶜ).vertexSet = G.vertexSet \ (↑H).vertexSet ∪ V(G, G.edgeSet \ (↑H).edgeSet)

source

@[simp]

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

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

source

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

Disjoint (↑H).edgeSet (↑Hᶜ).edgeSet

source

theorem Graph.Subgraph.mem_edgeSet_or_compl_edgeSet {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (H : G.Subgraph) (he : e ∈ G.edgeSet) :

e ∈ (↑H).edgeSet ∨ e ∈ (↑Hᶜ).edgeSet

source

@[simp]

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

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

source

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

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

source

@[simp]

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

H₁ᶜ ≤ H₂ ↔ G.vertexSet \ (↑H₁).vertexSet ⊆ (↑H₂).vertexSet ∧ G.edgeSet \ (↑H₁).edgeSet ⊆ (↑H₂).edgeSet

source

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

ofEdge G (G.edgeSet \ (↑H).edgeSet) ≤ Hᶜ

source

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

Set α

Equations

H.sep = (↑H).vertexSet ∩ V(G, G.edgeSet \ (↑H).edgeSet)

Instances For

source

@[simp]

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

x ∈ H.sep ↔ x ∈ (↑H).vertexSet ∧ ∃ e ∈ G.edgeSet \ (↑H).edgeSet, G.Inc e x

source

@[simp]

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

H.sep ⊆ (↑H).vertexSet

source

theorem Graph.Subgraph.sep_eq_vertexSet_inter_compl {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ : G.Subgraph} :

H₁.sep = (↑H₁).vertexSet ∩ (↑H₁ᶜ).vertexSet

source

@[simp]

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

H.sep ⊆ (↑Hᶜ).vertexSet

source

theorem Graph.Subgraph.inf_compl_eq_bot_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {H₁ : G.Subgraph} :

H₁ ⊓ H₁ᶜ = ⊥ ↔ (↑H₁).IsClosedSubgraph G

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_reducible]

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

PartialOrder G.ClosedSubgraph

Equations

Graph.ClosedSubgraph.instPartialOrder = { toPreorder := Subtype.preorder fun (H : Graph α β) => H.IsClosedSubgraph G, le_antisymm := ⋯ }

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

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_reducible]

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_reducible]

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_reducible]

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_reducible]

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

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

@[simp]

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

H ≠ ⊥ ↔ (↑H).vertexSet.Nonempty

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₂