Set Theory

Results named in Tau Ceti's TauCeti.SetTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe cardinality form of Silver's theorem #

A Borel equivalence relation on a standard Borel space has at most ℵ₀ or exactly 𝔠 classes.

Setoid.mk_quotient_le_aleph0_or_eq_continuum.{u_1} {X : Type u_1} [MeasurableSpace X]
  [StandardBorelSpace X] (E : Setoid X) (hE : MeasurableSet {p | E p.1 p.2}) :
  Cardinal.mk (Quotient E) ≤ Cardinal.aleph0 ∨ Cardinal.mk (Quotient E) = Cardinal.continuum

Lean

Formalized in Tau Ceti as Setoid.mk_quotient_le_aleph0_or_eq_continuum.

Sources

LeanSetoid.mk_quotient_le_aleph0_or_eq_continuum

Uses 1

Proof usesSilver's theorem

TheoremThe category route to Silver's theorem #

Let E be a Borel equivalence relation and φ a continuous map from Cantor space sending the edges of gSGraph S to E-inequivalent pairs. If S is dense, the range of φ carries a Cantor antichain for E.

Setoid.hasCantorAntichainOn_range_of_forall_gSGraph_adj.{u_1} {X : Type u_1} {S : Set (List Bool)}
  {φ : (ℕ → Bool) → X} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (E : Setoid X)
  (hE : MeasurableSet {p | E p.1 p.2}) (hS : TauCeti.DenseWords S) (hφ : Continuous φ)
  (hφE : ∀ ⦃y z : ℕ → Bool⦄, (TauCeti.gSGraph S).Adj y z → ¬E (φ y) (φ z)) :
  E.HasCantorAntichainOn (Set.range φ)

Lean

Formalized in Tau Ceti as Setoid.hasCantorAntichainOn_range_of_forall_gSGraph_adj.

Sources

LeanSetoid.hasCantorAntichainOn_range_of_forall_gSGraph_adj

Uses 3 · Used by 1

Proof usesThe Kuratowski–Ulam theorem · Miller's independence lemma · Mycielski's theorem

Used bySilver's theorem

TheoremThe Kechris–Solecki–Todorcevic G₀ dichotomy #

A simple graph on a Polish space whose edge relation is analytic has a measurable coloring by ℕ, or receives a continuous homomorphism from gZero, and not both.

SimpleGraph.g0_dichotomy.{u_1} {X : Type u_1} [TopologicalSpace X] [PolishSpace X]
  [MeasurableSpace X] [BorelSpace X] (G : SimpleGraph X)
  (hG : MeasureTheory.AnalyticSet {p | G.Adj p.1 p.2}) :
  Xor (∃ c, Measurable ⇑c) (∃ φ, Continuous ⇑φ)

Lean

Formalized in Tau Ceti as SimpleGraph.g0_dichotomy.

Sources

LeanSimpleGraph.g0_dichotomy

Uses 2

Proof usesThe Kechris–Solecki–Todorcevic lemma · Miller's independence lemma

TheoremThe Kechris–Solecki–Todorcevic lemma #

In a Hausdorff space with its Borel σ-algebra, an analytic independent set of an analytic relation is contained in a Borel independent set.

SetRel.exists_measurableSet_isIndependent_superset.{u_1} {X : Type u_1} {G : SetRel X X} {A : Set X}
  [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [BorelSpace X]
  (hG : MeasureTheory.AnalyticSet G) (hA : MeasureTheory.AnalyticSet A) (hind : G.IsIndependent A) :
  ∃ B, MeasurableSet B ∧ A ⊆ B ∧ G.IsIndependent B

Lean

Formalized in Tau Ceti as SetRel.exists_measurableSet_isIndependent_superset.

Sources

LeanSetRel.exists_measurableSet_isIndependent_superset

Used by 2

Used bySilver's theorem · The Kechris–Solecki–Todorcevic G₀ dichotomy

TheoremLusin–Sierpiński / Kunen–Martin boundedness theorem (relative form)#

Let s be an analytic subset of a topological space X and F : X → Descriptive.tree A a family of descriptive trees over a countable alphabet A : Type u. Suppose F x is well-founded for every x ∈ s and {x : s | u ∈ F x.1} is closed in the subspace s for every finite sequence u : List A. Then some countable ordinal β < ω₁ strictly bounds rank (F x) across all x ∈ s.

MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one.{u, u_1} {X : Type u_1} [TopologicalSpace X]
  {A : Type u} [Countable A] {s : Set X} (hs : MeasureTheory.AnalyticSet s)
  (F : X → ↥(Descriptive.tree A)) (hwf : ∀ x ∈ s, Descriptive.Tree.IsWellFounded (F x))
  (hcl : ∀ (u : List A), IsClosed {x | u ∈ F ↑x}) :
  ∃ β < Ordinal.omega 1, ∀ x ∈ s, Descriptive.Tree.rank (F x) < β

Lean

Formalized in Tau Ceti as MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one.

Other forms

Lusin–Sierpiński / Kunen–Martin boundedness theorem (ambient-closed form). Formalized in Tau Ceti as MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one_of_isClosed.

MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one_of_isClosed.{u, u_1} {X : Type u_1}
  [TopologicalSpace X] {A : Type u} [Countable A] {s : Set X} (hs : MeasureTheory.AnalyticSet s)
  (F : X → ↥(Descriptive.tree A)) (hwf : ∀ x ∈ s, Descriptive.Tree.IsWellFounded (F x))
  (hcl : ∀ (u : List A), IsClosed {x | u ∈ F x}) :
  ∃ β < Ordinal.omega 1, ∀ x ∈ s, Descriptive.Tree.rank (F x) < β

Sources

LeanMeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one · MeasureTheory.AnalyticSet.exists_treeRank_lt_omega_one_of_isClosed

TheoremMiller's independence lemma #

If every word extends to a word of S, then every non-meagre subset of Cantor space with the Baire property contains both ends of an oriented edge of orientedGS S.

TauCeti.exists_mem_orientedGS_of_not_isMeagre {S : Set (List Bool)} {A : Set (ℕ → Bool)}
  (hS : TauCeti.DenseWords S) (hA : BaireMeasurableSet A) (hn : ¬IsMeagre A) :
  ∃ a ∈ A, ∃ b ∈ A, (a, b) ∈ TauCeti.orientedGS S

Lean

Formalized in Tau Ceti as TauCeti.exists_mem_orientedGS_of_not_isMeagre.

Other forms

Miller's independence lemma, for the simple graph. Formalized in Tau Ceti as TauCeti.exists_gSGraph_adj_of_not_isMeagre.

TauCeti.exists_gSGraph_adj_of_not_isMeagre {S : Set (List Bool)} {A : Set (ℕ → Bool)}
  (hS : TauCeti.DenseWords S) (hA : BaireMeasurableSet A) (hn : ¬IsMeagre A) :
  ∃ a ∈ A, ∃ b ∈ A, (TauCeti.gSGraph S).Adj a b

Sources

LeanTauCeti.exists_mem_orientedGS_of_not_isMeagre · TauCeti.exists_gSGraph_adj_of_not_isMeagre

Used by 2

Used byThe category route to Silver's theorem · The Kechris–Solecki–Todorcevic G₀ dichotomy

TheoremThe perfect set theorem for analytic sets (Souslin)#

An uncountable analytic subset of a Hausdorff space contains the range of a continuous injection of Cantor space.

MeasureTheory.AnalyticSet.exists_nat_bool_injection_of_not_countable.{u} {X : Type u}
  [TopologicalSpace X] [T2Space X] {s : Set X} (hs : MeasureTheory.AnalyticSet s)
  (hunc : ¬s.Countable) : ∃ f, Set.range f ⊆ s ∧ Continuous f ∧ Function.Injective f

Lean

Formalized in Tau Ceti as MeasureTheory.AnalyticSet.exists_nat_bool_injection_of_not_countable.

Sources

LeanMeasureTheory.AnalyticSet.exists_nat_bool_injection_of_not_countable

TheoremSilver's theorem #

A Borel equivalence relation on a Polish space has countably many classes, or a Cantor antichain on the whole space: a continuous map of Cantor space sending distinct points to inequivalent points.

Setoid.silver_dichotomy.{u_1} {X : Type u_1} [TopologicalSpace X] [PolishSpace X]
  [MeasurableSpace X] [BorelSpace X] (E : Setoid X) (hE : MeasurableSet {p | E p.1 p.2}) :
  Countable (Quotient E) ∨ E.HasCantorAntichainOn Set.univ

Lean

Formalized in Tau Ceti as Setoid.silver_dichotomy.

Other forms

Silver's theorem in reducibility form. Formalized in Tau Ceti as Setoid.borelReducible_bot_iff_not_countable_quotient.

Setoid.borelReducible_bot_iff_not_countable_quotient.{u_1} {X : Type u_1} [MeasurableSpace X]
  [StandardBorelSpace X] (E : Setoid X) (hE : MeasurableSet {p | E p.1 p.2}) :
  ⊥.BorelReducible E ↔ ¬Countable (Quotient E)

Silver's theorem on a standard Borel space. Formalized in Tau Ceti as Setoid.silver_dichotomy_standardBorel.

Setoid.silver_dichotomy_standardBorel.{u_1} {X : Type u_1} [MeasurableSpace X]
  [StandardBorelSpace X] (E : Setoid X) (hE : MeasurableSet {p | E p.1 p.2}) :
  Countable (Quotient E) ∨ ∃ f, MeasurableEmbedding f ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬E (f a) (f b)

Sources

LeanSetoid.silver_dichotomy · Setoid.borelReducible_bot_iff_not_countable_quotient · Setoid.silver_dichotomy_standardBorel

Uses 2 · Used by 2

Proof usesThe category route to Silver's theorem · The Kechris–Solecki–Todorcevic lemma

Used bySilver's theorem relative to a Borel subset · The cardinality form of Silver's theorem

TheoremSilver's theorem relative to a Borel subset #

Let A be a Borel subset of a Polish space X, F a Borel equivalence relation on A, and R any equivalence relation on X whose restriction to A refines F. Then F has countably many classes, or A carries a Cantor antichain for R, continuous for the topology of X.

Setoid.countable_or_hasCantorAntichainOn_of_measurableSet.{u_1} {X : Type u_1} [TopologicalSpace X]
  [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {A : Set X} (hA : MeasurableSet A)
  (R : Setoid X) (F : Setoid ↑A) (hRF : ∀ (x y : ↑A), R ↑x ↑y → F x y)
  (hF : MeasurableSet {p | F p.1 p.2}) : Countable (Quotient F) ∨ R.HasCantorAntichainOn A

Lean

Formalized in Tau Ceti as Setoid.countable_or_hasCantorAntichainOn_of_measurableSet.

Sources

LeanSetoid.countable_or_hasCantorAntichainOn_of_measurableSet

Uses 2 · Used by 2

Proof usesThe perfect set theorem for Borel sets (Alexandrov–Hausdorff) · Silver's theorem

Used byMorley's dichotomy on the tier ℕ · Morley's theorem (cardinal form)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Set Theory

TheoremThe cardinality form of Silver's theorem#

Lean

Sources

TheoremThe category route to Silver's theorem#

Lean

Sources

TheoremThe Kechris–Solecki–Todorcevic G₀ dichotomy#

Lean

Sources

TheoremThe Kechris–Solecki–Todorcevic lemma#

Lean

Sources

TheoremLusin–Sierpiński / Kunen–Martin boundedness theorem (relative form)#

Lean

Other forms

Sources

TheoremMiller's independence lemma#

Lean

Other forms

Sources

TheoremThe perfect set theorem for analytic sets (Souslin)#

Lean

Sources

TheoremSilver's theorem#

Lean

Other forms

Sources

TheoremSilver's theorem relative to a Borel subset#

Lean

Sources

TheoremThe cardinality form of Silver's theorem #

TheoremThe category route to Silver's theorem #

TheoremThe Kechris–Solecki–Todorcevic G₀ dichotomy #

TheoremThe Kechris–Solecki–Todorcevic lemma #

TheoremMiller's independence lemma #

TheoremSilver's theorem #

TheoremSilver's theorem relative to a Borel subset #