/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 595
References:
[Er87] Erdős, Paul, Problems and results on set systems and hypergraphs. Extremal problems for finite sets (Visegrád, 1991), Bolyai Soc. Math. Stud. (1994), 217-227.
[Fo70] Folkman, Jon, Graphs with monochromatic complete subgraphs in every edge coloring. SIAM J. Appl. Math. (1970), 19:340-345.
[NeRo75] Nešetřil, Jaroslav and Rödl, Vojtěch, Type theory of partition problems of graphs. Recent advances in graph theory (Proc. Second Czechoslovak Sympos., Prague, 1974), Academia, Prague (1975), 405-412.
open SimpleGraph Setnamespace Erdos595def IsCountableUnionOfTriangleFree {V : Type*} (G : SimpleGraph V) : Prop :=
∃ H : ℕ → SimpleGraph V, (∀ i, (H i).CliqueFree 3) ∧ G = ⨆ i, H iErdős Problem 595 ($250): Is there an infinite graph $G$ which contains no $K_4$ and is not the union of countably many triangle-free graphs?
A problem of Erdős and Hajnal [Er87].
@[category research open, AMS 5]
theorem erdos_595 : answer(sorry) ↔
∃ (V : Type*) (_ : Infinite V) (G : SimpleGraph V),
G.CliqueFree 4 ∧ ¬IsCountableUnionOfTriangleFree G := ⊢ True ↔ ∃ V, ∃ (_ : Infinite V), ∃ G, G.CliqueFree 4 ∧ ¬IsCountableUnionOfTriangleFree G
All goals completed! 🐙
Folkman–Nešetřil–Rödl (finite version) [Fo70, NeRo75]: For every n ≥ 1, there exists a
graph G (on a finite vertex set) that contains no $K_4$ and whose edges cannot be covered by
n triangle-free graphs.
More precisely: for every n : ℕ with 1 ≤ n, there exist a finite type V and a graph
G : SimpleGraph V with:
G.CliqueFree 4 (no $K_4$), and
For every family H : Fin n → SimpleGraph V of triangle-free graphs, G ≠ ⨆ i, H i.
This is the finite analogue of Problem 595. The proofs of Folkman [Fo70] and Nešetřil–Rödl [NeRo75] give different explicit constructions.
@[category research solved, AMS 5]
theorem erdos_595.variants.folkman_finite : answer(True) ↔
∀ n : ℕ, 1 ≤ n →
∃ (V : Type*) (_ : Fintype V) (G : SimpleGraph V),
G.CliqueFree 4 ∧
∀ (H : Fin n → SimpleGraph V), (∀ i, (H i).CliqueFree 3) → G ≠ ⨆ i, H i := ⊢ True ↔
∀ (n : ℕ),
1 ≤ n → ∃ V x G, G.CliqueFree 4 ∧ ∀ (H : Fin n → SimpleGraph V), (∀ (i : Fin n), (H i).CliqueFree 3) → G ≠ ⨆ i, H i
-- Folkman [Fo70] and Nešetřil–Rödl [NeRo75]: explicit construction exists.
All goals completed! 🐙
Monotonicity: If G is a countable union of triangle-free graphs and H ≤ G (i.e., H is
a subgraph of G), then H is also a countable union of triangle-free graphs.
Proof: If G = ⨆ i, G_i with each G_i triangle-free, then H = ⨆ i, H ⊓ G_i.
Each H ⊓ G_i is triangle-free because it is a subgraph of G_i.
V:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vhab:H.Adj a bhabG:∃ i, (f i).Adj a b⊢ ∃ i, H.Adj a b ∧ (f i).Adj a b
V:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vhab:H.Adj a bi:ℕhi:(f i).Adj a b⊢ ∃ i, H.Adj a b ∧ (f i).Adj a b
All goals completed! 🐙
V:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:V⊢ (∃ i, H.Adj a b ∧ (f i).Adj a b) → H.Adj a b V:Type u_1G:SimpleGraph VH:SimpleGraph VhH:H ≤ Gf:ℕ → SimpleGraph Vhf_free:∀ (i : ℕ), (f i).CliqueFree 3hf_eq:G = ⨆ i, f ia:Vb:Vi:ℕhHab:H.Adj a bright✝:(f i).Adj a b⊢ H.Adj a b
All goals completed! 🐙
Triangle-free graphs are trivially countable unions of triangle-free graphs: if G is
already triangle-free, then G = ⨆ i : ℕ, G_i where G_0 = G and G_i = ⊥ for i ≥ 1.
@[category textbook, AMS 5]
theorem erdos_595.variants.triangle_free_is_union
{V : Type*} (G : SimpleGraph V) (hG : G.CliqueFree 3) :
IsCountableUnionOfTriangleFree G := V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3⊢ IsCountableUnionOfTriangleFree G
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕ⊢ ((fun i ↦ if i = 0 then G else ⊥) i).CliqueFree 3V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3⊢ G = ⨆ i, (fun i ↦ if i = 0 then G else ⊥) i
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕ⊢ ((fun i ↦ if i = 0 then G else ⊥) i).CliqueFree 3 V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:i = 0⊢ ((fun i ↦ if i = 0 then G else ⊥) i).CliqueFree 3V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:¬i = 0⊢ ((fun i ↦ if i = 0 then G else ⊥) i).CliqueFree 3
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:i = 0⊢ ((fun i ↦ if i = 0 then G else ⊥) i).CliqueFree 3 All goals completed! 🐙
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3i:ℕh:¬i = 0⊢ ((fun i ↦ if i = 0 then G else ⊥) i).CliqueFree 3 All goals completed! 🐙
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3⊢ G = ⨆ i, (fun i ↦ if i = 0 then G else ⊥) i V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b ↔ (⨆ i, (fun i ↦ if i = 0 then G else ⊥) i).Adj a b
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b ↔ ∃ i, (if i = 0 then G else ⊥).Adj a b
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b → ∃ i, (if i = 0 then G else ⊥).Adj a bV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ (∃ i, (if i = 0 then G else ⊥).Adj a b) → G.Adj a b
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ G.Adj a b → ∃ i, (if i = 0 then G else ⊥).Adj a b V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vhab:G.Adj a b⊢ ∃ i, (if i = 0 then G else ⊥).Adj a b
exact ⟨0, V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vhab:G.Adj a b⊢ (if 0 = 0 then G else ⊥).Adj a b All goals completed! 🐙⟩
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:V⊢ (∃ i, (if i = 0 then G else ⊥).Adj a b) → G.Adj a b V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a b⊢ G.Adj a b
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:i = 0⊢ G.Adj a bV:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:¬i = 0⊢ G.Adj a b
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:i = 0⊢ G.Adj a b V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕh:i = 0hi:G.Adj a b⊢ G.Adj a b; All goals completed! 🐙
V:Type u_1G:SimpleGraph VhG:G.CliqueFree 3a:Vb:Vi:ℕhi:(if i = 0 then G else ⊥).Adj a bh:¬i = 0⊢ G.Adj a b All goals completed! 🐙
The complete graph ⊤ on ℕ is a countable union of triangle-free graphs: we decompose
it into the family of star graphs {H_m}_{m : ℕ}, where H_m is the graph with edges {m, n}
for all n ≠ m. Each star is triangle-free (any two non-center vertices share no edge within
the star), and their union covers all edges of ⊤.
Proof sketch (star triangle-free): If {a, b, c} were a triangle in H_m, then each of
the three edges {a, b}, {a, c}, {b, c} would pass through m. In particular, from
{a, b} we get a = m or b = m; from {b, c} we get b = m or c = m. Case analysis
shows that two vertices must equal m, contradicting the triangle having three distinct vertices.
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}⊢ False
-- Extract membership in s.
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ s⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ s⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ s⊢ False
-- Each pair is adjacent in H_m.
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:(fromRel fun a b ↦ a = m ∨ b = m).Adj a b⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:(fromRel fun a b ↦ a = m ∨ b = m).Adj a bhac_adj:(fromRel fun a b ↦ a = m ∨ b = m).Adj a c⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:(fromRel fun a b ↦ a = m ∨ b = m).Adj a bhac_adj:(fromRel fun a b ↦ a = m ∨ b = m).Adj a chbc_adj:(fromRel fun a b ↦ a = m ∨ b = m).Adj b c⊢ False
-- fromRel_adj: (fromRel r).Adj x y ↔ x ≠ y ∧ (r x y ∨ r y x)
-- For r x y = (x = m ∨ y = m): r x y ∨ r y x simplifies to x = m ∨ y = m.
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)⊢ False
-- Extract "a = m or b = m", "a = m or c = m", "b = m or c = m".
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)ham_or_bm:a = m ∨ b = m⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)ham_or_bm:a = m ∨ b = mham_or_cm:a = m ∨ c = m⊢ False
m:ℕs:Finset ℕhs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = m ∨ b = m).Adjhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shab_adj:a ≠ b ∧ ((a = m ∨ b = m) ∨ b = m ∨ a = m)hac_adj:a ≠ c ∧ ((a = m ∨ c = m) ∨ c = m ∨ a = m)hbc_adj:b ≠ c ∧ ((b = m ∨ c = m) ∨ c = m ∨ b = m)ham_or_bm:a = m ∨ b = mham_or_cm:a = m ∨ c = mhbm_or_cm:b = m ∨ c = m⊢ False
-- Case analysis: whichever vertex equals m forces another to equal m as well,
-- contradicting distinctness.
s:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a_1 b ↦ a_1 = a ∨ b = a).Adjhab_adj:a ≠ b ∧ ((a = a ∨ b = a) ∨ b = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:b ≠ c ∧ ((b = a ∨ c = a) ∨ c = a ∨ b = a)ham_or_cm:a = a ∨ c = ahbm_or_cm:b = a ∨ c = a⊢ Falses:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b_1 ↦ a = b ∨ b_1 = b).Adjhab_adj:a ≠ b ∧ ((a = b ∨ b = b) ∨ b = b ∨ a = b)hac_adj:a ≠ c ∧ ((a = b ∨ c = b) ∨ c = b ∨ a = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:a = b ∨ c = bhbm_or_cm:b = b ∨ c = b⊢ False
s:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a_1 b ↦ a_1 = a ∨ b = a).Adjhab_adj:a ≠ b ∧ ((a = a ∨ b = a) ∨ b = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:b ≠ c ∧ ((b = a ∨ c = a) ∨ c = a ∨ b = a)ham_or_cm:a = a ∨ c = ahbm_or_cm:b = a ∨ c = a⊢ False -- a = m
s:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ shc:c ∈ shab:b ≠ bhac:b ≠ chs_eq:s = {b, b, c}ha:b ∈ shs_clique:(↑s).Pairwise (fromRel fun a b_1 ↦ a = b ∨ b_1 = b).Adjhab_adj:b ≠ b ∧ ((b = b ∨ b = b) ∨ b = b ∨ b = b)hac_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:b = b ∨ c = b⊢ Falses:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ shc:c ∈ shab:c ≠ bhac:c ≠ chs_eq:s = {c, b, c}ha:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = c ∨ b = c).Adjhab_adj:c ≠ b ∧ ((c = c ∨ b = c) ∨ b = c ∨ c = c)hac_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbc_adj:b ≠ c ∧ ((b = c ∨ c = c) ∨ c = c ∨ b = c)ham_or_cm:c = c ∨ c = c⊢ False
s:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ shc:c ∈ shab:b ≠ bhac:b ≠ chs_eq:s = {b, b, c}ha:b ∈ shs_clique:(↑s).Pairwise (fromRel fun a b_1 ↦ a = b ∨ b_1 = b).Adjhab_adj:b ≠ b ∧ ((b = b ∨ b = b) ∨ b = b ∨ b = b)hac_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:b = b ∨ c = b⊢ False All goals completed! 🐙 -- b = a = m
s:Finset ℕhs_card:s.card = 3b:ℕc:ℕhbc:b ≠ chb:b ∈ shc:c ∈ shab:c ≠ bhac:c ≠ chs_eq:s = {c, b, c}ha:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = c ∨ b = c).Adjhab_adj:c ≠ b ∧ ((c = c ∨ b = c) ∨ b = c ∨ c = c)hac_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbc_adj:b ≠ c ∧ ((b = c ∨ c = c) ∨ c = c ∨ b = c)ham_or_cm:c = c ∨ c = c⊢ False All goals completed! 🐙 -- c = a = m
s:Finset ℕhs_card:s.card = 3a:ℕb:ℕc:ℕhab:a ≠ bhac:a ≠ chbc:b ≠ chs_eq:s = {a, b, c}ha:a ∈ shb:b ∈ shc:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b_1 ↦ a = b ∨ b_1 = b).Adjhab_adj:a ≠ b ∧ ((a = b ∨ b = b) ∨ b = b ∨ a = b)hac_adj:a ≠ c ∧ ((a = b ∨ c = b) ∨ c = b ∨ a = b)hbc_adj:b ≠ c ∧ ((b = b ∨ c = b) ∨ c = b ∨ b = b)ham_or_cm:a = b ∨ c = bhbm_or_cm:b = b ∨ c = b⊢ False -- b = m
s:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ shc:c ∈ shab:a ≠ ahbc:a ≠ chs_eq:s = {a, a, c}hb:a ∈ shs_clique:(↑s).Pairwise (fromRel fun a_1 b ↦ a_1 = a ∨ b = a).Adjhab_adj:a ≠ a ∧ ((a = a ∨ a = a) ∨ a = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbm_or_cm:a = a ∨ c = a⊢ Falses:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ shc:c ∈ shab:a ≠ chbc:c ≠ chs_eq:s = {a, c, c}hb:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = c ∨ b = c).Adjhab_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hac_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hbc_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbm_or_cm:c = c ∨ c = c⊢ False
s:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ shc:c ∈ shab:a ≠ ahbc:a ≠ chs_eq:s = {a, a, c}hb:a ∈ shs_clique:(↑s).Pairwise (fromRel fun a_1 b ↦ a_1 = a ∨ b = a).Adjhab_adj:a ≠ a ∧ ((a = a ∨ a = a) ∨ a = a ∨ a = a)hac_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbc_adj:a ≠ c ∧ ((a = a ∨ c = a) ∨ c = a ∨ a = a)hbm_or_cm:a = a ∨ c = a⊢ False All goals completed! 🐙 -- a = b = m, so a = m and b = m, contradiction
s:Finset ℕhs_card:s.card = 3a:ℕc:ℕhac:a ≠ cha:a ∈ shc:c ∈ shab:a ≠ chbc:c ≠ chs_eq:s = {a, c, c}hb:c ∈ shs_clique:(↑s).Pairwise (fromRel fun a b ↦ a = c ∨ b = c).Adjhab_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hac_adj:a ≠ c ∧ ((a = c ∨ c = c) ∨ c = c ∨ a = c)hbc_adj:c ≠ c ∧ ((c = c ∨ c = c) ∨ c = c ∨ c = c)hbm_or_cm:c = c ∨ c = c⊢ False All goals completed! 🐙 -- c = b = m, so b = c, contradiction
⊢ ⊤ = ⨆ i, (fun m ↦ fromRel fun a b ↦ a = m ∨ b = m) i -- The union ⨆ m, H_m equals ⊤.
a:ℕb:ℕ⊢ ⊤.Adj a b ↔ (⨆ i, (fun m ↦ fromRel fun a b ↦ a = m ∨ b = m) i).Adj a b
a:ℕb:ℕ⊢ a ≠ b ↔ ∃ i, a ≠ b ∧ ((a = i ∨ b = i) ∨ b = i ∨ a = i)
-- Goal: a ≠ b ↔ ∃ m, a ≠ b ∧ ((a = m ∨ b = m) ∨ (b = m ∨ a = m))
All goals completed! 🐙
The complete graph ⊤ on Fin 4 is not $K_4$-free: ⊤ on Fin 4 equals the complete
graph $K_4$, so it contains $K_4$ as a subgraph and is not $K_4$-free.
This sanity check confirms the $K_4$-free hypothesis of Problem 595 is non-trivial.
⊢ completeGraph (Fin 4) ⊑ ⊤
All goals completed! 🐙
Reformulation via edge colourings: A graph G is a countable union of triangle-free graphs
if and only if there is a colouring of the edges of G by ℕ such that no monochromatic
triangle exists.
More precisely: IsCountableUnionOfTriangleFree G is equivalent to the existence of a map
c : G.edgeSet → ℕ such that for each n : ℕ, the subgraph of edges coloured n is triangle-free.
V:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSetn:ℕx:Vy:Vhxy:s(x, y) ∈ {e | ∃ (h : e ∈ G.edgeSet), (fun e ↦ ⋯.choose) ⟨e, h⟩ = n} ∧ x ≠ y⊢ (H n).Adj x y
V:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSetn:ℕx:Vy:Vright✝:x ≠ yh_mem:s(x, y) ∈ G.edgeSeth_eq:(fun e ↦ ⋯.choose) ⟨s(x, y), h_mem⟩ = n⊢ (H n).Adj x y
-- h_eq : (hcov ⟨s(x,y), h_mem⟩).choose = n
-- choose_spec gives s(x,y) ∈ (H (choose)).edgeSet; after rewriting with h_eq, in H n.
V:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSetn:ℕx:Vy:Vright✝:x ≠ yh_mem:s(x, y) ∈ G.edgeSeth_eq:(fun e ↦ ⋯.choose) ⟨s(x, y), h_mem⟩ = nhspec:↑⟨s(x, y), h_mem⟩ ∈ (H ⋯.choose).edgeSet⊢ (H n).Adj x y
V:Type u_1G:SimpleGraph VH:ℕ → SimpleGraph VhH_free:∀ (i : ℕ), (H i).CliqueFree 3hH_eq:G = ⨆ i, H ihcov:∀ (e : ↑G.edgeSet), ∃ i, ↑e ∈ (H i).edgeSetn:ℕx:Vy:Vright✝:x ≠ yh_mem:s(x, y) ∈ G.edgeSeth_eq:(fun e ↦ ⋯.choose) ⟨s(x, y), h_mem⟩ = nhspec:s(x, y) ∈ (H n).edgeSet⊢ (H n).Adj x y
All goals completed! 🐙
V:Type u_1G:SimpleGraph V⊢ (∃ c, ∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3) →
IsCountableUnionOfTriangleFree G -- (←): Given c : G.edgeSet → ℕ, define H n = fromEdgeSet {e | ∃ h, c ⟨e,h⟩ = n}.
-- This is EdgeLabeling.labelGraph c n, so ⨆ n, H n = G by iSup_labelGraph.
V:Type u_1G:SimpleGraph Vc:↑G.edgeSet → ℕhc:∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3⊢ IsCountableUnionOfTriangleFree G
V:Type u_1G:SimpleGraph Vc:↑G.edgeSet → ℕhc:∀ (n : ℕ), (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}).CliqueFree 3⊢ G = ⨆ i, (fun n ↦ fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), c ⟨e, h⟩ = n}) i
-- G = ⨆ n, (labelGraph c n) follows from EdgeLabeling.iSup_labelGraph.
All goals completed! 🐙end Erdos595