Open coloring axiom

StructureOpen coloring of a topological space#✓fully proved

Let \(X\) be a topological space. A set \(K \subseteq X \times X\) of ordered pairs is an open coloring of \(X\) if \(K\) is open in the product topology, symmetric (\((x, y) \in K\) implies \((y, x) \in K\)) and irreflexive (\((x, x) \notin K\) for every \(x \in X\)).

structure IsOpenColoring {X : Type} [TopologicalSpace X] (K : Set (X × X)) : Prop where
  isOpen : IsOpen K
  symm : ∀ x y : X, (x, y) ∈ K → (y, x) ∈ K
  irrefl : ∀ x : X, (x, x) ∉ K

Used by 1

Used byOpen coloring axiom

DefinitionHomogeneous set for a coloring#✓fully proved

Let \(X\) be a set and \(K \subseteq X \times X\). A set \(H \subseteq X\) is \(K\)-homogeneous if \((x, y) \in K\) for all distinct \(x, y \in H\).

def IsColoringHomogeneous {X : Type} (K : Set (X × X)) (H : Set X) : Prop :=
  H.Pairwise fun x y => (x, y) ∈ K

Used by 1

Used byOpen coloring axiom

DefinitionFree set for a coloring#✓fully proved

Let \(X\) be a set and \(K \subseteq X \times X\). A set \(H \subseteq X\) is \(K\)-free if \((x, y) \notin K\) for all \(x, y \in H\).

def IsColoringFree {X : Type} (K : Set (X × X)) (H : Set X) : Prop :=
  ∀ x ∈ H, ∀ y ∈ H, (x, y) ∉ K

Used by 1

Used byOpen coloring axiom

DefinitionOpen coloring axiom#✓fully proved

Todorcevic's Open Coloring Axiom: for every open coloring of a second-countable space, either there is an uncountable homogeneous set, or the space is a countable union of free sets.

def OpenColoringAxiom : Prop :=
  ∀ (X : Type) [TopologicalSpace X] [SecondCountableTopology X] (K : Set (X × X)),
    IsOpenColoring K →
      (∃ H : Set X, ¬ H.Countable ∧ IsColoringHomogeneous K H) ∨
      (∃ F : ℕ → Set X, (⋃ n, F n) = Set.univ ∧ ∀ n, IsColoringFree K (F n))

Uses 3

Statement usesFree set for a coloring · Homogeneous set for a coloring · Open coloring of a topological space

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.