SeparableQuotientNegative

Definition

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

CH is the defined proposition that the cardinality of the real numbers equals aleph-one, the continuum hypothesis. For a real or complex scalar field 𝕜 (any RCLike field) and a normed 𝕜-vector space X in universe u, HasSeparableQuotient(𝕜,X) means that there exist a normed 𝕜-vector space Y in the same universe that is complete, topologically separable and not finite-dimensional over 𝕜, together with a bounded 𝕜-linear surjection T from X onto Y. SQ(𝕜) is the separable quotient assertion, stated as a defined proposition rather than an established theorem: for every complete normed 𝕜-vector space X in universe u that is not finite-dimensional, HasSeparableQuotient(𝕜,X) holds, so every infinite-dimensional Banach space admits a bounded linear map onto an infinite-dimensional separable Banach space. The universe u is arbitrary, and the block states no relationship between CH and SQ.

Definition code

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SeparableQuotientNegative.lean; bytes 16..888
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib

namespace OAI

namespace SeparableQuotient

open MeasureTheory Cardinal

universe u

/-- The continuum hypothesis. -/
def CH : Prop := Cardinal.mk ℝ = Cardinal.aleph 1

/-- A bounded linear surjection onto an infinite-dimensional separable Banach space. -/
def HasSeparableQuotient (𝕜 : Type) [RCLike 𝕜]
    (X : Type u) [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Prop :=
  ∃ (Y : Type u) (_ : NormedAddCommGroup Y) (_ : NormedSpace 𝕜 Y),
    CompleteSpace Y ∧ TopologicalSpace.SeparableSpace Y ∧
      (¬ FiniteDimensional 𝕜 Y) ∧ ∃ T : X →L[𝕜] Y, Function.Surjective T

/-- The separable quotient assertion at an arbitrary ambient universe. -/
def SQ (𝕜 : Type) [RCLike 𝕜] : Prop :=
  ∀ (X : Type u) [NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X],
    (¬ FiniteDimensional 𝕜 X) → HasSeparableQuotient 𝕜 X



end SeparableQuotient
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/SeparableQuotientNegative.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph