Dense and continuous completion of a linear order

Let α be a linear order.

• DedekindCut.continuous_principal: the map DedekindCut.principal : α → DedekindCut α that embeds α in its Dedekind completion is continuous for the order topologies.
• Order.Fill α: this is a type with a dense linear order endowed with a continuous order-embedding Order.Fill.some of α. It is defined as a subtype of α × ℚ and its order is induced by the lexicographic order.
• Order.Fill.some: the order embedding α ↪o Order.Fill α given by a ↦ (a, 0).
• Order.Fill.continuous_some: the map ⇑Order.Fill.some is continuous for the order topologies.
• Order.exists_dense_continuous_completion: any linear order embeds continuously (for the order topologies) into a dense and complete linear order. The linearly ordered type provided by the proof is given by the Dedekind completion of Order.Fill α, although the user does not need to know that.

theorem DedekindCut.continuous_principal {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)] : Continuous fun (a : α) => principal a

@[reducible, inline]

abbrev Order.Fill (α : Type u_2) [LinearOrder α] : Type u_2

A dense linear order into which α embeds continuously, formed by "filling in" the blanks.

Equations

• Order.Fill α = { x : Lex (α × ℚ) // (Order.IsSuccPrelimit (ofLex x).1 → 0 ≤ (ofLex x).2) ∧ (Order.IsPredPrelimit (ofLex x).1 → (ofLex x).2 ≤ 0) }

@[implicit_reducible]

instance Order.Fill.instTopologicalSpace {α : Type u_1} [LinearOrder α] : TopologicalSpace (Fill α)

Equations

• Order.Fill.instTopologicalSpace = Preorder.topology (Order.Fill α)

instance Order.Fill.instOrderTopology {α : Type u_1} [LinearOrder α] : OrderTopology (Fill α)

def Order.Fill.some {α : Type u_1} [LinearOrder α] : α ↪o Fill α

A continuous embedding of α into Fill α.

Equations

• Order.Fill.some = { toFun := fun (x : α) => ⟨toLex (x, 0), ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

instance Order.Fill.instDenselyOrdered {α : Type u_1} [LinearOrder α] : DenselyOrdered (Fill α)

theorem Order.Fill.continuous_some {α : Type u_1} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] : Continuous ⇑some

theorem Order.exists_dense_continuous_completion (α : Type u) [LinearOrder α] [TopologicalSpace α] [OrderTopology α] : ∃ (β : Type u) (x : CompleteLinearOrder β) (_ : DenselyOrdered β) (x_2 : TopologicalSpace β) (_ : OrderTopology β) (ι : α ↪o β), Continuous ⇑ι

Every linear order embeds continuously in a dense complete linear order.