Square principle

DefinitionSquare sequence#✓fully proved

Jensen's square principle sequence: C = (C_α : α < κ⁺) is a □_κ-sequence: for every limit α < κ⁺, C_α is club in α of order type at most κ, and the family coheres — C_β = C_α ∩ β whenever β is a limit point of C_α.

def IsSquareSequence.{u} (κ : Cardinal.{u})
      (C : (Order.succ κ).ord.ToType → Set ((Order.succ κ).ord.ToType)) : Prop :=
    ∀ a : (Order.succ κ).ord.ToType, Order.IsSuccLimit a →
      (C a ⊆ Set.Iio a) ∧
      (∀ b < a, ∃ c ∈ C a, b < c) ∧
      (∀ b < a, (C a ∩ Set.Iio b).Nonempty → IsLUB (C a ∩ Set.Iio b) b → b ∈ C a) ∧
      Ordinal.type (α := ↥(C a)) (· < ·) ≤ κ.ord ∧
      (∀ b, (C a ∩ Set.Iio b).Nonempty → IsLUB (C a ∩ Set.Iio b) b →
        C b = C a ∩ Set.Iio b)

Used by 1

Used byJensen's square principle

DefinitionJensen's square principle#✓fully proved

□_κ: a □_κ-sequence exists

def Square.{u} (κ : Cardinal.{u}) : Prop :=
    ∃ C : (Order.succ κ).ord.ToType → Set ((Order.succ κ).ord.ToType), IsSquareSequence κ C

Uses 1

Statement usesSquare sequence

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.