FormalConjectures.ErdosProblems.«593»

/-
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 FormalConjecturesUtil

Erdős Problem 593

References:

erdosproblems.com/593

[EGH75] Erdős, Paul and Galvin, Fred and Hajnal, András, On set-systems having large chromatic number and not containing prescribed subsystems. Infinite and finite sets (Colloq., Keszthely, 1973; dedicated to P. Erdős on his 60th birthday), Vol. I. Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 425–513.

[Er95d] Erdős, Paul, Some of my favourite problems in various branches of combinatorics. Matematiche (Catania) 47 (1992), no. 2, 231–240 (1995).


open Cardinal Set SimpleGraph


namespace Erdos593

Erdős Problem 593 ($500): Characterize those finite 3-uniform hypergraphs which appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$.

A natural conjectural characterization, recorded here, is that the obligatory finite 3-uniform hypergraphs are exactly the 2-colorable ones (Property B). The forward direction (IsObligatory → IsTwoColorable) and converse (IsTwoColorable → IsObligatory) are stated as separate variants below; in the graph case ($r = 2$), Erdős–Galvin–Hajnal [EGH75] proved the analogous result (obligatory ⇔ bipartite).

@[category research open, AMS 5]
theorem declaration uses 'sorry'erdos_593 : answer(sorry) ↔
    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
      IsObligatory F ↔ F.IsTwoColorable := by⊢ True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorable
  sorryAll goals completed! 🐙

Erdős Problem 593 — Necessary direction: Every obligatory finite 3-uniform hypergraph is 2-colorable.

This is the natural necessary condition for the conjectural characterization in erdos_593: if a finite 3-uniform hypergraph F is not 2-colorable, one expects to construct a hypergraph with large chromatic number that contains no copy of F.

@[category research open, AMS 5]
theorem declaration uses 'sorry'erdos_593.variants.obligatory_implies_two_colorable : answer(sorry) ↔
    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
      IsObligatory F → F.IsTwoColorable := by⊢ True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorable
  sorryAll goals completed! 🐙

Erdős Problem 593 — Sufficient direction: Every finite 2-colorable 3-uniform hypergraph is obligatory.

This is the converse direction of the erdos_593 characterization: if 2-colorability matches the graph-case characterization (bipartite ⇔ obligatory), then every 2-colorable finite 3-uniform hypergraph must appear in every 3-uniform hypergraph of chromatic number $> \aleph_0$.

Together with erdos_593.variants.obligatory_implies_two_colorable, this implies erdos_593.

@[category research open, AMS 5]
theorem declaration uses 'sorry'erdos_593.variants.two_colorable_implies_obligatory : answer(sorry) ↔
    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
      F.IsTwoColorable → IsObligatory F := by⊢ True ↔ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F
  sorryAll goals completed! 🐙

Conjunction of the two open implications gives the conjectured characterization: if both obligatory_implies_two_colorable and two_colorable_implies_obligatory hold, then the characterization conjectured in erdos_593 (IsObligatory F ↔ F.IsTwoColorable) follows by elementary Iff manipulation.

@[category test, AMS 5]
theorem erdos_593.variants.implications_combine
    (h₁ : ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
            IsObligatory F → F.IsTwoColorable)
    (h₂ : ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
            F.IsTwoColorable → IsObligatory F) :
    ∀ (W : Type) [Fintype W] (F : ThreeUniformHypergraph W),
      IsObligatory F ↔ F.IsTwoColorable := byh₁:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorableh₂:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory F⊢ ∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorable
  intro W _h₁:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorableh₂:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory FW:Typeinst✝:Fintype W⊢ ∀ (F : ThreeUniformHypergraph W), IsObligatory F ↔ F.IsTwoColorable Fh₁:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), IsObligatory F → F.IsTwoColorableh₂:∀ (W : Type) [inst : Fintype W] (F : ThreeUniformHypergraph W), F.IsTwoColorable → IsObligatory FW:Typeinst✝:Fintype WF:ThreeUniformHypergraph W⊢ IsObligatory F ↔ F.IsTwoColorable
  exact ⟨h₁ W F, h₂ W F⟩All goals completed! 🐙

Graph analogue — bipartite graphs are obligatory (Erdős–Galvin–Hajnal [EGH75]): For the 2-uniform (graph) case, a graph of chromatic cardinal $> \aleph_0$ must contain all finite bipartite graphs. Specifically, for every finite bipartite graph F and every graph G with chromatic cardinal $> \aleph_0$, there is a graph embedding from F into G.

This uses Nonempty (F ↪g G) (graph embedding), aligned with the injective vertex map used in the hypergraph Appears definition.

@[category research solved, AMS 5]
theorem declaration uses 'sorry'erdos_593.variants.graph_case_bipartite_obligatory :
    answer(True) ↔
    ∀ (V : Type*) (G : SimpleGraph V),
      ℵ₀ < G.chromaticCardinal →
      ∀ (W : Type*) [Fintype W] (F : SimpleGraph W), F.IsBipartite →
        Nonempty (F ↪g G) := by⊢ True ↔
  ∀ (V : Type u_1) (G : SimpleGraph V),
    ℵ₀ < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → Nonempty (F ↪g G)
  simp only [true_iff]⊢ ∀ (V : Type u_1) (G : SimpleGraph V),
  ℵ₀ < G.chromaticCardinal → ∀ (W : Type u_2) [Fintype W] (F : SimpleGraph W), F.IsBipartite → Nonempty (F ↪g G)
  -- This is the Erdős–Galvin–Hajnal theorem [EGH75].
  sorryAll goals completed! 🐙

Graph analogue — no odd cycle is obligatory (Erdős–Galvin–Hajnal [EGH75]): For every odd $k \geq 3$, there exists a graph with chromatic cardinal $\aleph_1$ that contains no cycle of length $k$. This shows the class of obligatory graphs is strictly smaller than all finite graphs.

@[category research solved, AMS 5]
theorem declaration uses 'sorry'erdos_593.variants.graph_case_no_odd_cycle :
    answer(True) ↔
    ∀ k : ℕ, Odd k → 3 ≤ k →
      ∃ (V : Type*) (G : SimpleGraph V),
        G.chromaticCardinal = ℵ_ 1 ∧
        IsEmpty (cycleGraph k →g G) := by⊢ True ↔ ∀ (k : ℕ), Odd k → 3 ≤ k → ∃ V G, G.chromaticCardinal = ℵ_ 1 ∧ IsEmpty (cycleGraph k →g G)
  simp only [true_iff]⊢ ∀ (k : ℕ), Odd k → 3 ≤ k → ∃ V G, G.chromaticCardinal = ℵ_ 1 ∧ IsEmpty (cycleGraph k →g G)
  -- This is the Erdős–Galvin–Hajnal theorem [EGH75].
  sorryAll goals completed! 🐙

Vertices must be uncountable: Every 3-uniform hypergraph with chromatic cardinal $> \aleph_0$ must have an uncountable vertex set.

Proof: If V is countable, there exists an injection φ : V → ℕ. Using distinct natural numbers as colors gives a proper coloring, so $\chi(H) \leq #\mathbb{N} = \aleph_0$, contradicting $\chi(H) > \aleph_0$.

@[category textbook, AMS 5]
theorem erdos_593.variants.uncountable_vertices_if_large_chromatic
    {V : Type} (H : ThreeUniformHypergraph V) (hχ : ℵ₀ < H.chromaticCardinal) :
    ¬ Countable V := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ ¬Countable V
  intro hcountV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable V⊢ False
  -- Since V is countable, there is an injection φ : V → ℕ.
  obtain ⟨φ, hφ⟩ := Countable.exists_injective_nat VV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φ⊢ False
  -- The injection φ is a proper coloring using ℕ as the color type:
  -- each edge has card 3, so we can extract two distinct vertices with distinct images.
  have hprop : H.IsProperColoring φ := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ ¬Countable V
    intro e heV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φe:Finset Vhe:e ∈ H.edges⊢ ∃ u ∈ e, ∃ v ∈ e, φ u ≠ φ v
    -- Extract 3 distinct elements from e using H.uniform.
    have hcard : e.card = 3 := H.uniform e heV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φe:Finset Vhe:e ∈ H.edgeshcard:e.card = 3 := H.uniform e he⊢ ∃ u ∈ e, ∃ v ∈ e, φ u ≠ φ v
    -- Since e.card = 3 ≥ 2, there exist two distinct elements u ≠ v in e.
    have hge : 1 < e.card := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ ¬Countable V omegaAll goals completed! 🐙
    obtain ⟨u, hu, v, hv, huv⟩ := Finset.one_lt_card.mp hgeV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φe:Finset Vhe:e ∈ H.edgeshcard:e.card = 3 := H.uniform e hehge:1 < e.card := Decidable.byContradiction fun a => uncountable_vertices_if_large_chromatic._proof_1 e hcard au:Vhu:u ∈ ev:Vhv:v ∈ ehuv:u ≠ v⊢ ∃ u ∈ e, ∃ v ∈ e, φ u ≠ φ v
    exact ⟨u, hu, v, hv, fun heq => huv (hφ heq)⟩All goals completed! 🐙
  -- So χ(H) ≤ #ℕ = ℵ₀.
  have hle : H.chromaticCardinal ≤ ℵ₀ := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ ¬Countable V
    apply csInf_leh₁V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φhprop:H.IsProperColoring φ := 
  fun e he =>
    have hcard := H.uniform e he;
    have hge := Decidable.byContradiction fun a => uncountable_vertices_if_large_chromatic._proof_1 e hcard a;
    Exists.casesOn (Finset.one_lt_card.mp hge) fun u h =>
      And.casesOn h fun hu right =>
        Exists.casesOn right fun v h =>
          And.casesOn h fun hv huv => Exists.intro u ⟨hu, Exists.intro v ⟨hv, fun heq => huv (hφ heq)⟩⟩⊢ BddBelow {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f}h₂V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φhprop:H.IsProperColoring φ := 
  fun e he =>
    have hcard := H.uniform e he;
    have hge := Decidable.byContradiction fun a => uncountable_vertices_if_large_chromatic._proof_1 e hcard a;
    Exists.casesOn (Finset.one_lt_card.mp hge) fun u h =>
      And.casesOn h fun hu right =>
        Exists.casesOn right fun v h =>
          And.casesOn h fun hv huv => Exists.intro u ⟨hu, Exists.intro v ⟨hv, fun heq => huv (hφ heq)⟩⟩⊢ ℵ₀ ∈ {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f}
    ·h₁V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φhprop:H.IsProperColoring φ := 
  fun e he =>
    have hcard := H.uniform e he;
    have hge := Decidable.byContradiction fun a => uncountable_vertices_if_large_chromatic._proof_1 e hcard a;
    Exists.casesOn (Finset.one_lt_card.mp hge) fun u h =>
      And.casesOn h fun hu right =>
        Exists.casesOn right fun v h =>
          And.casesOn h fun hv huv => Exists.intro u ⟨hu, Exists.intro v ⟨hv, fun heq => huv (hφ heq)⟩⟩⊢ BddBelow {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f} -- The set {κ | ∃ C, #C = κ ∧ ∃ f, proper} is bounded below by 0.
      exact ⟨0, fun _ ⟨_, _, _, _⟩ => Cardinal.zero_le _⟩All goals completed! 🐙
    ·h₂V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhcount:Countable Vφ:V → ℕhφ:Function.Injective φhprop:H.IsProperColoring φ := 
  fun e he =>
    have hcard := H.uniform e he;
    have hge := Decidable.byContradiction fun a => uncountable_vertices_if_large_chromatic._proof_1 e hcard a;
    Exists.casesOn (Finset.one_lt_card.mp hge) fun u h =>
      And.casesOn h fun hu right =>
        Exists.casesOn right fun v h =>
          And.casesOn h fun hv huv => Exists.intro u ⟨hu, Exists.intro v ⟨hv, fun heq => huv (hφ heq)⟩⟩⊢ ℵ₀ ∈ {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f} exact ⟨ℕ, Cardinal.mk_nat, φ, hprop⟩All goals completed! 🐙
  exact absurd (lt_of_lt_of_le hχ hle) (lt_irrefl _)All goals completed! 🐙

No hyperedges implies chromatic cardinal ≤ 1: A 3-uniform hypergraph with no edges can be properly colored with a single color, so its chromatic cardinal is at most 1. In particular, $\chi(H) > \aleph_0$ implies H has at least one hyperedge.

@[category textbook, AMS 5]
theorem erdos_593.variants.nonempty_edges_if_large_chromatic
    {V : Type} (H : ThreeUniformHypergraph V) (hχ : ℵ₀ < H.chromaticCardinal) :
    H.edges.Nonempty := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ H.edges.Nonempty
  by_contra hemptyV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:¬H.edges.Nonempty⊢ False
  push_neg at hemptyV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅⊢ False
  -- H has no edges (hempty : H.edges = ∅), so any coloring is proper.
  have hprop : H.IsProperColoring (fun _ : V => (0 : Fin 1)) := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ H.edges.Nonempty
    intro e heV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅e:Finset Vhe:e ∈ H.edges⊢ ∃ u ∈ e, ∃ v ∈ e, (fun x => 0) u ≠ (fun x => 0) v
    rw [hempty] at heV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅e:Finset Vhe:e ∈ ∅⊢ ∃ u ∈ e, ∃ v ∈ e, (fun x => 0) u ≠ (fun x => 0) v
    exact (Set.mem_empty_iff_false e).mp he |>.elimAll goals completed! 🐙
  -- Hence χ(H) ≤ 1 < ℵ₀.
  have hle : H.chromaticCardinal ≤ 1 := byV:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ H.edges.Nonempty
    apply csInf_leh₁V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x => 0 := fun e he => False.elim ((mem_empty_iff_false e).mp (Eq.mp (congrArg (fun _a => e ∈ _a) hempty) he))⊢ BddBelow {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f}h₂V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x => 0 := fun e he => False.elim ((mem_empty_iff_false e).mp (Eq.mp (congrArg (fun _a => e ∈ _a) hempty) he))⊢ 1 ∈ {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f}
    ·h₁V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x => 0 := fun e he => False.elim ((mem_empty_iff_false e).mp (Eq.mp (congrArg (fun _a => e ∈ _a) hempty) he))⊢ BddBelow {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f} exact ⟨0, fun _ ⟨_, _, _, _⟩ => Cardinal.zero_le _⟩All goals completed! 🐙
    ·h₂V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x => 0 := fun e he => False.elim ((mem_empty_iff_false e).mp (Eq.mp (congrArg (fun _a => e ∈ _a) hempty) he))⊢ 1 ∈ {κ | ∃ C, #C = κ ∧ ∃ f, H.IsProperColoring f} refine ⟨Fin 1, ?_, fun _ => 0, hprop⟩h₂V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x => 0 := fun e he => False.elim ((mem_empty_iff_false e).mp (Eq.mp (congrArg (fun _a => e ∈ _a) hempty) he))⊢ #(Fin 1) = 1
      simpAll goals completed! 🐙
  have h1le : (1 : Cardinal) ≤ ℵ₀ := le_of_lt Cardinal.one_lt_aleph0V:TypeH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalhempty:H.edges = ∅hprop:H.IsProperColoring fun x => 0 := fun e he => False.elim ((mem_empty_iff_false e).mp (Eq.mp (congrArg (fun _a => e ∈ _a) hempty) he))hle:H.chromaticCardinal ≤ 1 := 
  csInf_le
    (Exists.intro 0 fun x x_1 =>
      match x_1 with
      | Exists.intro w ⟨left, Exists.intro w_1 h⟩ => Cardinal.zero_le x)
    (Exists.intro (Fin 1)
      ⟨of_eq_true
          (Eq.trans
            (congrArg (fun x => x = 1)
              (Eq.trans (mk_fintype (Fin 1)) (Eq.trans (congrArg Nat.cast Fintype.card_unique) Nat.cast_one)))
            (eq_self 1)),
        Exists.intro (fun x => 0) hprop⟩)h1le:1 ≤ ℵ₀ := le_of_lt one_lt_aleph0⊢ False
  exact absurd (lt_of_lt_of_le hχ (hle.trans h1le)) (lt_irrefl _)All goals completed! 🐙

Monotonicity of the obligatory property: If F₁ appears in F₂ and F₂ is obligatory, then F₁ is also obligatory.

Proof: For any H with $\chi(H) > \aleph_0$, since F₂ is obligatory, F₂ appears in H via some injection φ₂. Since F₁ appears in F₂ via φ₁, the composition φ₂ ∘ φ₁ witnesses that F₁ appears in H.

@[category textbook, AMS 5]
theorem erdos_593.variants.obligatory_monotone
    {W₁ W₂ : Type} [Fintype W₁] [Fintype W₂] [DecidableEq W₂]
    {F₁ : ThreeUniformHypergraph W₁} {F₂ : ThreeUniformHypergraph W₂}
    (h12 : F₁.Appears F₂) (hObl : IsObligatory F₂) :
    IsObligatory F₁ := byW₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂h12:F₁.Appears F₂hObl:IsObligatory F₂⊢ IsObligatory F₁
  intro V _hVW₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂h12:F₁.Appears F₂hObl:IsObligatory F₂V:Type_hV:DecidableEq V⊢ ∀ (H : ThreeUniformHypergraph V), ℵ₀ < H.chromaticCardinal → F₁.Appears H HW₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂h12:F₁.Appears F₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph V⊢ ℵ₀ < H.chromaticCardinal → F₁.Appears H hχW₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂h12:F₁.Appears F₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinal⊢ F₁.Appears H
  obtain ⟨φ₂, hφ₂_inj, hφ₂_edge⟩ := hObl V H hχW₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂h12:F₁.Appears F₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalφ₂:W₂ → Vhφ₂_inj:Function.Injective φ₂hφ₂_edge:∀ e ∈ F₂.edges, Finset.image φ₂ e ∈ H.edges⊢ F₁.Appears H
  obtain ⟨φ₁, hφ₁_inj, hφ₁_edge⟩ := h12W₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalφ₂:W₂ → Vhφ₂_inj:Function.Injective φ₂hφ₂_edge:∀ e ∈ F₂.edges, Finset.image φ₂ e ∈ H.edgesφ₁:W₁ → W₂hφ₁_inj:Function.Injective φ₁hφ₁_edge:∀ e ∈ F₁.edges, Finset.image φ₁ e ∈ F₂.edges⊢ F₁.Appears H
  refine ⟨φ₂ ∘ φ₁, hφ₂_inj.comp hφ₁_inj, fun e he => ?_⟩W₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalφ₂:W₂ → Vhφ₂_inj:Function.Injective φ₂hφ₂_edge:∀ e ∈ F₂.edges, Finset.image φ₂ e ∈ H.edgesφ₁:W₁ → W₂hφ₁_inj:Function.Injective φ₁hφ₁_edge:∀ e ∈ F₁.edges, Finset.image φ₁ e ∈ F₂.edgese:Finset W₁he:e ∈ F₁.edges⊢ Finset.image (φ₂ ∘ φ₁) e ∈ H.edges
  -- e.image (φ₂ ∘ φ₁) = (e.image φ₁).image φ₂ by Finset.image_image
  have heq : e.image (φ₂ ∘ φ₁) = (e.image φ₁).image φ₂ := byW₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂h12:F₁.Appears F₂hObl:IsObligatory F₂⊢ IsObligatory F₁
    rw [Finset.image_image]All goals completed! 🐙
  rw [heq]W₁:TypeW₂:Typeinst✝²:Fintype W₁inst✝¹:Fintype W₂inst✝:DecidableEq W₂F₁:ThreeUniformHypergraph W₁F₂:ThreeUniformHypergraph W₂hObl:IsObligatory F₂V:Type_hV:DecidableEq VH:ThreeUniformHypergraph Vhχ:ℵ₀ < H.chromaticCardinalφ₂:W₂ → Vhφ₂_inj:Function.Injective φ₂hφ₂_edge:∀ e ∈ F₂.edges, Finset.image φ₂ e ∈ H.edgesφ₁:W₁ → W₂hφ₁_inj:Function.Injective φ₁hφ₁_edge:∀ e ∈ F₁.edges, Finset.image φ₁ e ∈ F₂.edgese:Finset W₁he:e ∈ F₁.edgesheq:Finset.image (φ₂ ∘ φ₁) e = Finset.image φ₂ (Finset.image φ₁ e) := Eq.mpr (id (congrArg (fun _a => Finset.image (φ₂ ∘ φ₁) e = _a) Finset.image_image)) (Eq.refl (Finset.image (φ₂ ∘ φ₁) e))⊢ Finset.image φ₂ (Finset.image φ₁ e) ∈ H.edges
  exact hφ₂_edge _ (hφ₁_edge e he)All goals completed! 🐙

The empty hypergraph is trivially obligatory: The 3-uniform hypergraph on PEmpty (no vertices, no edges) appears in every hypergraph via the empty injection.

This degenerate case confirms the definition is well-formed.

@[category textbook, AMS 5]
theorem erdos_593.variants.empty_hypergraph_obligatory :
    IsObligatory (W := PEmpty) ⟨∅, fun _ h => (Set.mem_empty_iff_false _).mp h |>.elim⟩ := by⊢ IsObligatory { edges := ∅, uniform := ⋯ }
  intro V _hVV:Type_hV:DecidableEq V⊢ ∀ (H : ThreeUniformHypergraph V), ℵ₀ < H.chromaticCardinal → { edges := ∅, uniform := ⋯ }.Appears H HV:Type_hV:DecidableEq VH:ThreeUniformHypergraph V⊢ ℵ₀ < H.chromaticCardinal → { edges := ∅, uniform := ⋯ }.Appears H _hχV:Type_hV:DecidableEq VH:ThreeUniformHypergraph V_hχ:ℵ₀ < H.chromaticCardinal⊢ { edges := ∅, uniform := ⋯ }.Appears H
  exact ⟨IsEmpty.elim inferInstance, Function.injective_of_subsingleton _,
    fun _ h => (Set.mem_empty_iff_false _).mp h |>.elim⟩All goals completed! 🐙


end Erdos593