Alphabeta MathPersonal research
Article items · 02 — A finite set with $n$ elements has exactly $\binom{n}{2}$ two-element subsets, and $2\binom{n}{2} = n(n-1)$
Presents 29 items from the article and its immediate prerequisites, covering published library prerequisites and dependency levels 0–2.
1 · Prerequisites
- C(n, k) k! (n-k)! = n! for k ≤ n; hence C(n, k) k! = n^k̲, the quotient n!/(k!(n-k)!) is a natural number, and C(n, k) = C(n, n-k)
- The set [A]ᵏ of k-element subsets and the binomial coefficient C(n, k) := | [n]ᵏ|
- The factorial n! and the falling factorial n^k̲, defined by recursion in ℕ
- The cardinality | A| of a finite set
- Laws of finite sums and products in ℕ, and ι(∑_k<n aₖ) = ∑_k<n ι(aₖ)
- The canonical natural ι(n) = n · 1_F of a field
- Multiplication of natural numbers
- Multiplication is commutative
- Zero and one under multiplication
- Order on the natural numbers
- Trichotomy of the order on ℕ
- Field
- Ordered field
- The natural numbers ℕ (von Neumann)
- The principle of mathematical induction
- Discreteness: σ(n) is the immediate successor
- The von Neumann naturals form a Peano system
- Left successor law for addition
- Left identity for addition
- r-uniform hypergraphs and complete balanced r-partite r-graphs K⁽ʳ⁾_s,…,s
- A finite simple graph is a finite vertex set together with a set of two-element vertex subsets
- The Cartesian product A × B := { z ∈ P(P(A ∪ B)) : ∃ a ∈ A ∃ b ∈ B z = (a,b) }
- Maria Axenovich and Annette Karrer, High girth hypergraphs with unavoidable monochromatic or rainbow edges, arXiv:1607.06600v2 · Section 1, cycle and girth paragraph immediately before Theorem 1
- Connected graphs and connected components defined by the existence of vertex paths
- The connected components of a graph partition its vertex set and are its maximal connected subgraphs
- Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges
- Subgraphs, induced subgraphs and spanning subgraphs
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
- A bridge as an edge whose deletion increases the number of connected components
- lvertP(A)| = 2^| A| for finite A
- A subset of a finite set is finite, with | B| ≤ | A|, and equality holds if and only if B = A
- The product rule: | A × B| = | A| | B|, and |∏_i<m Aᵢ| = ∏_i<m| Aᵢ|
- ≤ is a linear order on ℕ
- Injection, surjection, bijection
- The union ⋃ x of a set, and the binary union a ∪ b := ⋃ {a,b}
- An indexed family (Aᵢ)_i ∈ I is a function with domain I; {Aᵢ : i ∈ I} is its range
- ⋃_i ∈ I Aᵢ := ⋃ {Aᵢ : i ∈ I}, and ⋂_i ∈ I Aᵢ := ⋂ {Aᵢ : i ∈ I} for I ≠ ∅
- A function is a relation f with (a,b) ∈ f and (a,c) ∈ f implying b = c; f : A → B, the value f(a), domain and codomain
- Graph isomorphisms, automorphisms and graph complements
- Induced embeddings and induced copies of a graph
- The sum rule: a finite disjoint union is finite with | A ∪ B| = | A| + | B| and |⋃_i ∈ I Aᵢ| = ∑_i ∈ I| Aᵢ|, and a sum over a finite index set splits along a partition
- (a,b) = (c,d) if and only if a = c and b = d
- Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree
- The Axiom Schema of Separation: for each formula φ, ∀ p̄ ∀ x ∃ y ∀ z (z ∈ y ↔ (z ∈ x ∧ φ(z,p̄)))
- The Axiom of Extensionality: ∀ x ∀ y (∀ z (z ∈ x ↔ z ∈ y) → x = y)
- Cliques, independent sets, clique number and independence number
- The recursion theorem
- The power set P(x) = { z : z ⊆ x }
- Empty and complete graphs, complete bipartite graphs, and the convention that Pₙ and Cₙ have n vertices
- The difference a ∖ b, the symmetric difference a △ b, and the complement X ∖ a relative to a set X
- Every nonzero natural number is a successor
- On ℕ the order is membership: m < n ⟺ m ∈ n
- G[W]=Ḡ[W] for every vertex set W
- Set partitions and blocks
- For relations R and S and a set A, the collections { (b,a) : (a,b) ∈ R }, { (a,c) : ∃ b ((a,b) ∈ R ∧ (b,c) ∈ S) } and { (a,b) ∈ R : a ∈ A } are sets
- If | A| > k| B| then every f : A → B has a fibre with more than k elements, and for nonempty B some fibre has at least ⌈ | A| / | B|⌉ elements
- Division with remainder for any nonzero divisor: for a ∈ ℤ and b ≠ 0 there are unique q, r ∈ ℤ with a = qb + r and 0 ≤ r < |b|
- The complete connection of two disjoint graphs
- Addition is cancellative
- Addition is commutative
2 · Logical flowchart
Arrows show item dependencies. A grouped prerequisite node points to items that use one or more of its members; their exact links are listed above.
3 · Items
TheoremLibrary prerequisite
A finite set with n elements has exactly C(n, 2) two-element subsets, and 2C(n, 2) = n(n-1)
TheoremLibrary prerequisite
The well-ordering principle
DefinitionDependency level 0
Berge cycles, incidence graphs and girth
DefinitionDependency level 0
Cutvertices, 2-connected pieces and nontrivial blocks
DefinitionDependency level 0
Graph realisations with possibly different hyperedge pieces
DefinitionDependency level 0
Ordinary embeddings as injections preserving edges
DefinitionDependency level 0
Tagged graph families with anticomplete parts
DefinitionDependency level 0
Unrestricted finite colourings and used palettes
LemmaDependency level 0
Clique and independence duality under complementation
LemmaDependency level 0
Complement of a disconnected graph is connected
LemmaDependency level 0
Recursion for deterministic finite graph updates
LemmaDependency level 0
Independence is monotone under induced embeddings
DefinitionDependency level 1
Graph and colouring conventions
DefinitionDependency level 1
Neighbourhood attachments indexed by induced embeddings
DefinitionDependency level 1
Weak hypergraph colourings with singleton boundary
LemmaDependency level 1
Berge girth at least three forces linearity
LemmaDependency level 1
Block containment and monotonicity under subgraphs
LemmaDependency level 1
Complementation transports induced copies on fixed vertices
LemmaDependency level 1
Connected subgraphs cannot cross anticomplete parts
LemmaDependency level 1
Transport, restriction and relabelling of finite colourings
LemmaDependency level 1
Rigidity of mutual ordinary embeddings
LemmaDependency level 1
Finite colour-class capacity and prescribed partitions
LemmaDependency level 1
Independence numbers of disjoint families and complete joins
LemmaDependency level 1
Nonempty remainder after deleting an independent set
LemmaDependency level 1
Linear realisations preserve induced pieces
LemmaDependency level 1
Completing a restricted target with universal clique vertices
DefinitionDependency level 2
The disjoint multiple qA
DefinitionDependency level 2
Edge-Ramsey class terminology in the motivation
DefinitionDependency level 2