Closure properties of graph classes

Lax871432.ClosureProperties · concepts/Lax871432/ClosureProperties.lean · lax-871432

definition

Loading review…

Natural Language Statement

Definition

Five closure properties of a class $\mathcal{F}$ of finite simple graphs.

$\mathcal{F}$ is closed under taking summands if $F_1 + F_2 \in \mathcal{F}$ implies $F_1 \in \mathcal{F}$ and $F_2 \in \mathcal{F}$ , where $+$ denotes disjoint union, and union-closed if conversely $F_1, F_2 \in \mathcal{F}$ implies $F_1 + F_2 \in \mathcal{F}$ . It is minor-closed if every minor of a member is a member.

It is closed under taking induced subgraphs if every induced subgraph of a member is a member, and closed under contracting edges if every graph obtained from a member by contracting edges is a member.

Concept map

4 concepts; 5 descendants hidden

100%

Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 4 of this submission's paper

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Sum
2	import Mathlib.Data.Finite.Sum
3	import Lax68.GraphMinors
4	import Lax871432.Contractions
5	import Lax871432.GraphClasses
6
7	/-!
8	---
9	title: Closure properties of graph classes
10	type: definition
11	---
12	Five closure properties of a class $\mathcal{F}$ of finite simple graphs.
13
14	$\mathcal{F}$ is closed under taking summands if $F_1 + F_2 \in \mathcal{F}$ implies
15	$F_1 \in \mathcal{F}$ and $F_2 \in \mathcal{F}$ , where $+$ denotes disjoint union, and
16	union-closed if conversely $F_1, F_2 \in \mathcal{F}$ implies
17	$F_1 + F_2 \in \mathcal{F}$ . It is minor-closed if every minor of a member is a member.
18
19	It is closed under taking induced subgraphs if every induced subgraph of a member is a
20	member, and closed under contracting edges if every graph obtained from a member by contracting edges is
21	a member.
22
23	-/
24
25	open Lax871432.Contractions Lax871432.GraphClasses
26
27	namespace Lax871432.ClosureProperties
28
29	/-- `𝓕` is closed under taking summands if both summands of a disjoint union in the class
30	are themselves in the class. -/
31	def IsSummandClosed (𝓕 : GraphClass) : Prop :=
32	∀ {V W : Type} [Finite V] [Finite W] (F₁ : SimpleGraph V) (F₂ : SimpleGraph W),
33	𝓕.Mem (F₁ ⊕g F₂) → 𝓕.Mem F₁ ∧ 𝓕.Mem F₂
34
35	/-- `𝓕` is union-closed if the disjoint union of two members is a member. -/
36	def IsUnionClosed (𝓕 : GraphClass) : Prop :=
37	∀ {V W : Type} [Finite V] [Finite W] (F₁ : SimpleGraph V) (F₂ : SimpleGraph W),
38	𝓕.Mem F₁ → 𝓕.Mem F₂ → 𝓕.Mem (F₁ ⊕g F₂)
39
40	/-- `𝓕` is closed under taking induced subgraphs if every induced subgraph of a member is a
41	member. -/
42	def IsInducedSubgraphClosed (𝓕 : GraphClass) : Prop :=
43	∀ {V : Type} [Finite V] (F : SimpleGraph V) (U : Set V), 𝓕.Mem F → 𝓕.Mem (F.induce U)
44
45	/-- `𝓕` is closed under contracting edges if every quotient of a member by a partition into
46	connected parts is a member. -/
47	def IsContractionClosed (𝓕 : GraphClass) : Prop :=
48	∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} (K : SimpleGraph W),
49	IsContraction K F → 𝓕.Mem F → 𝓕.Mem K
50
51	/-- `𝓕` is minor-closed if every minor of a member is a member. -/
52	def IsMinorClosed (𝓕 : GraphClass) : Prop :=
53	∀ {V W : Type} [Finite V] [Finite W] {F : SimpleGraph V} (K : SimpleGraph W),
54	Lax68.GraphMinors.IsMinor K F → 𝓕.Mem F → 𝓕.Mem K
55
56	end Lax871432.ClosureProperties
57

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Closure properties of graph classes

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments