PR summary cb39573f93

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

./scripts/reporting/technical-debt-metrics.sh pr_summary

What's the theorem you're trying to prove? Every linear order with the order topology embeds via a continuous map into a dense complete linear order?

Yes, but I need that embedding to be continuous for the order topologies. Then the lex product with Q doesn't work, and I believe i'll have to fill the holes but nothing more. (I updated the above description.)

I believe Dedekind.principal should always be continuous. You should be able to prove this by showing principal ⁻¹' Iio x = ⋃ y ∈ x.left, Iio (principal y), and likewise for Ioi. Also, the Dedekind completion of a dense order is dense. So that reduces the problem to embedding a linear order into a dense linear order continuously.

Embedding α into α ×ₗ ℚ doesn't work directly, but I think you can salvage it by taking a subtype instead. Say that your embedding maps x into toLex (x, 0). My idea is this: if x does not have a predecessor, remove all elements toLex (x, y) with y < 0 from the subtype. If x has no successor, remove all elements toLex (x, y) with 0 < y. I believe this subtype of α ×ₗ ℚ should be dense, and the embedding fun x ↦ toLex (x, 0) will be continuous.

In other words, you're adding a copy of ℚ in between any two consecutive elements.

Exactly, that's what I meant with “filling the holes”.

I find it easier (the formalization will say so, or not) to define an adequate Sigma type.

This is one fourth the length of your code :)

/-
Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Violeta Hernández Palacios, Antoine Chambert-Loir
-/
module

public import Mathlib.Data.Prod.Lex
public import Mathlib.Order.SuccPred.Limit
public import Mathlib.Topology.Order.Basic

import Mathlib.Algebra.Order.Field.Basic

@[expose] public section

namespace Order

variable {α : Type*} [LinearOrder α]

/-- A dense linear order into which α embeds continuously, formed by "filling in" the blanks. -/
abbrev Fill (α : Type*) [LinearOrder α] : Type _ :=
  {x : α ×ₗ ℚ //
    (IsSuccPrelimit (ofLex x).1 → 0 ≤ (ofLex x).2) ∧
    (IsPredPrelimit (ofLex x).1 → (ofLex x).2 ≤ 0) }

namespace Fill

instance [TopologicalSpace α] [OrderTopology α] : TopologicalSpace (Fill α) :=
  Preorder.topology _

instance [TopologicalSpace α] [OrderTopology α] : OrderTopology (Fill α) :=
  ⟨rfl⟩

/-- A continuous embedding of `α` into `Fill α`. -/
def some : α ↪o Fill α where
  toFun x := ⟨toLex (x, 0), by simp⟩
  inj' _ := by simp
  map_rel_iff' := by simp [Prod.Lex.toLex_le_toLex']

instance : DenselyOrdered (Fill α) where
  dense := by
    simp only [ofLex_toLex, Subtype.forall, Prod.Lex.lt_iff, Subtype.mk_lt_mk,
      Lex.forall, Prod.forall]
    rintro x q ⟨hx₁, hx₂⟩ y r ⟨hy₁, hy₂⟩ (h | ⟨rfl, h⟩)
    · by_cases hx : IsPredPrelimit x
      · obtain ⟨z, hz, hz'⟩ := hx.lt_iff_exists_lt.1 h
        use some z
        simp [some, Prod.Lex.lt_iff, hz', hz]
      obtain ⟨s, hs⟩ := exists_gt (max 0 q)
      rw [max_lt_iff] at hs
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · simp [hx, hs.1.le]
      · simp [Prod.Lex.lt_iff, hs.2, h]
    · obtain ⟨s, hs, hs'⟩ := exists_between h
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · grind [ofLex_toLex]
      · simp [Prod.Lex.lt_iff, hs, hs']

theorem continuous_some [TopologicalSpace α] [OrderTopology α] : Continuous (X := α) some := by
  simp only [OrderTopology.continuous_iff, ofLex_toLex, Subtype.forall, Lex.forall, Prod.forall]
  refine fun x q ⟨hx₁, hx₂⟩ ↦ ⟨?_, ?_⟩
  · obtain hq | hq := le_or_gt 0 q
    · convert isOpen_Ioi (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := (not_isSuccPrelimit_iff_exists_covBy _).1 <| mt hx₁ hq.not_ge
      convert isOpen_Ioi (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_right
  · obtain hq | hq := le_or_gt q 0
    · convert isOpen_Iio (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := (not_isPredPrelimit_iff_exists_covBy _).1 <| mt hx₂ hq.not_ge
      convert isOpen_Iio (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_left

end Fill
end Order

It's shorter but it does less, although this “less” (holes, etc.) might be uninteresting, and I'm not so happy with the going through Lex, I feel it unnatural.

I think everything outside of Order.Fill and the continuous_principal theorem would make a good self-contained PR.
What about Order.Hole?

It's shorter but it does less, although this “less” (holes, etc.) might be uninteresting, and I'm not so happy with the going through Lex, I feel it unnatural.

What else do you need it to do? Isn't the core result "any linear order embeds continuously into a dense linear order"?

I'm more interested into formalizing the how and the why than the what. It's OK, the core result is there.

Both of our constructions are ultimately isomorphic, so I don't see what distinction you're making.

I spent way too long trying to build something withe the flexibility of Antoine's approach as well as the conciseness of Violeta's, but this is not a huge success.

One thing to note is that Antoine's construction also works for densifying a partial order, as long as the order relation on holes compares both the left and the right components (which is still more natural, and in the linearly ordered case it's the same).

I think a reasonable middle ground (to keep some flexibility while still allowing for a more direct approach) would be to fill all holes with a single order. Then I would define Fill in the same way Antoine does (an inductive type is probably more natural to use), but pull back the order relation from an appropriate Lex (which means that you get most properties for free, except for continuity which is really specific to the situation).

How does this sound ? Antoine, do you have any reason to believe that the flexibility of putting a different order at different holes could matter for some application ?

One thing to note is that Antoine's construction also works for densifying a partial order.

The theorem that any order embeds in a dense order (not necessarily continuously) is trivial, since you can just take the lex product with the rationals (or any other dense nonempty order). The key property here is continuity, but the order topology doesn't really make sense in a partial order (it is well-defined, but rarely if ever the topology you actually want to put on it).