An analytic non-Borel subset of ℝ: the image of the Baire-space witness under the continuous injection. Analyticity transfers along the continuous image; non-Borelness transfers back along the injective preimage.
∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A
- DeclMeasureTheory.exists_analyticSet_not_measurableSet_realDeclaration kindtheorem
∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A
- DeclMeasureTheory.exists_analyticSet_not_measurableSetDeclaration kindtheorem
An analytic non-Borel subset of Baire space: the projection of the diagonal witness.
∃ A, MeasureTheory.AnalyticSet A ∧ ¬MeasurableSet A
- DeclMeasureTheory.exists_closed_proj_not_measurableSetDeclaration kindtheorem
A closed set with a non-Borel projection. Diagonalize the universal closed set of
(ℕ → ℕ) × (ℕ → ℕ): were the projection Borel, its complement would be analytic, hence the projection of a closed set, hence a section of the universal set — and evaluating that section at its own parameter is contradictory.∃ D, IsClosed D ∧ ¬MeasurableSet {x | ∃ y, (x, y) ∈ D} - DeclMeasureTheory.exists_closed_universal_sectionsDeclaration kindtheorem
A universal closed set. Every second-countable space
Xcarries a closed subset ofX × (ℕ → ℕ)whose sections run through all closed subsets ofX: enumerate a countable basis together with∅, and let the parameter select which basis elements to exclude.∀ (X : Type u_1) [inst : TopologicalSpace X] [SecondCountableTopology X], ∃ S, IsClosed S ∧ ∀ (C : Set X), IsClosed C → ∃ y, {x | (x, y) ∈ S} = C - DeclMeasureTheory.embedBaireReal_injectiveDeclaration kindtheorem
Function.Injective MeasureTheory.embedBaireReal
- DeclMeasureTheory.baireMarkerBits_injectiveDeclaration kindtheorem
Function.Injective MeasureTheory.baireMarkerBits
- DeclMeasureTheory.baireMarkers_strictMonoDeclaration kindtheorem
∀ (x : ℕ → ℕ), StrictMono (MeasureTheory.baireMarkers x)
- DeclMeasureTheory.continuous_embedBaireRealDeclaration kindtheorem
Continuous MeasureTheory.embedBaireReal
- DeclMeasureTheory.continuous_cantorFunction_oneThirdDeclaration kindtheorem
Continuous (Cardinal.cantorFunction (1 / 3))
- DeclMeasureTheory.continuous_baireMarkerBitsDeclaration kindtheorem
Continuous MeasureTheory.baireMarkerBits
- DefinitionMeasureTheory.baireMarkerBitsdef
The marker bits: the indicator stream of the marker set.
(ℕ → ℕ) → ℕ → Bool
- DefinitionMeasureTheory.baireMarkersdef
The marker sequence of
x : ℕ → ℕ: the strictly increasing sequencen + 1 + ∑_{k ≤ n} x k, whose successive gaps encodex.(ℕ → ℕ) → ℕ → ℕ
- DefinitionMeasureTheory.embedBaireRealdef
The embedding of Baire space into
ℝ: marker bits into the base-3 expansion.(ℕ → ℕ) → ℝ
Verification
- Replay
- accepted
- Axioms
- Classical.choiceQuot.soundpropext
- Statement identity
- not-applicable
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- design-lab@5802df4 · initial
- Frozen export
- 17a477359fda
- Verified
- 2026-09-24T00:00:00Z