Pi.Lex complete linear order

Stream: maths

[Violeta Hernández]

Suppose a is well-ordered and b is a complete linear order. Does it follow that a -> b (with the lexicographic ordering) is a complete linear order? Do we have this in Mathlib? If not, how do we prove it?

[Yaël Dillies]

a embeds into a → b, so you definitely need a to be complete too

[Violeta Hernández]

Well-order with top, then

[Violeta Hernández]

My actual example is WithTop Ordinal -> SignType in case that's relevant

[Aaron Liu]

Yes it follows, but I'm not aware of anything in mathlib

[Aaron Liu]

Yaël Dillies said:

a embeds into a → b

Not necessarily

[Aaron Liu]

not with the lex order

[Yaël Dillies]

Oh yes, sorry, I was confusing with ∑ₗ _ : a, b

[Edward van de Meent]

i think you might be able to do it if b has elements b1 < b2, by mapping x to fun y => if y < x then b2 else b1?

[Aaron Liu]

huh

[Aaron Liu]

oh

[Aaron Liu]

yeah that probably works

[Edward van de Meent]

it at the very least preserves <

[Edward van de Meent]

i'm not sure the other direction holds tho...

[Aaron Liu]

well it's linear

[Edward van de Meent]

ah yes of course

[Edward van de Meent]

so it can't in general be an embedding

[Edward van de Meent]

because not all well-orders are linear

[Aaron Liu]

well-orders are linear

[Aaron Liu]

well-founded relations are not necessarily linear

[Edward van de Meent]

ah, i was under the mistaken impression that wellorders are wellfounded orders

[Edward van de Meent]

in the case where a is linearly ordered, it is true that this is an embedding

[Aaron Liu]

wellorders are wellfounded linear orders

[Aaron Liu]

that is, linear orders that are docs#WellFoundedLT

[Aaron Liu]

it says so in the docstring for docs#IsWellOrder

[Edward van de Meent]

sure, but i didn't read that because the name seems descriptive enough to assume otherwise

[Edward van de Meent]

anywho, i understand the difference now.

[Violeta Hernández]

Aaron Liu said:

Yes it follows, but I'm not aware of anything in mathlib

Lol the reason I ask is because I wonder if your proof can be simplified and put into Mathlib in a more general case

[Aaron Liu]

my proof isn't for lex though

[Aaron Liu]

it's for a subtype of lex

[Aaron Liu]

I don't see how this would transfer to the subtype so I would still have to prove it again

[Aaron Liu]

I think I can probably generalize to CompleteLattice (Lex ((a : α) → β a)) when we have LinearOrder α and WellFoundedLT α and ∀ a, CompleteLattice (β a)

[Aaron Liu]

oh and I do see how I might be able to transfer to the subtype

[Violeta Hernández]

Aaron Liu said:

it's for a subtype of lex

Wait, the complete order on the subtype isn't just the one inherited from the order?

[Aaron Liu]

Violeta Hernández said:

Aaron Liu said:

it's for a subtype of lex

Wait, the complete order on the subtype isn't just the one inherited from the order?

not always

[Violeta Hernández]

Huh

[Aaron Liu]

only sometimes

[Violeta Hernández]

Do you have an example?

[Violeta Hernández]

(context for everyone else, the subtype is sequences where the pre image of {0} is upper closed)

[Aaron Liu]

take WithTop (WithTop Nat) and let the subtype be · ≠ WithTop.some ⊤

[Violeta Hernández]

Oh well yeah

[Aaron Liu]

then the sup of the natural numbers is different

[Violeta Hernández]

I mean, does it not transfer for our specific subtype

[Aaron Liu]

it does for our specific one I think

[Violeta Hernández]

nevermind counterexample doesn't work

[Violeta Hernández]

I think I have a relatively simple construction for the infimum

[Violeta Hernández]

Take a set $S$ of functions $f : \alpha \to \beta$, define $T_i = \{f(i) : f \in S\}$. Let $i \in \alpha$ be the least index with $\inf T_i \notin T_i$. Then the infimum is the function $f$ with $f(j) = \inf T_j$ for $j \le i$ and $f(j) = \top$ otherwise.

[Violeta Hernández]

@Aaron Liu Does this seem correct? It definitely does seem simpler than what you had; this is what I meant when I called ordinal induction a "noob trap".

[Aaron Liu]

no that doesn't work

[Violeta Hernández]

Darn :frown:

[Violeta Hernández]

Counterexample?

[Aaron Liu]

your order is the cantor set Lex (ℕ → Bool) and your set is {toLex fun n => n == 0, toLex fun n => n == 1}, the infimum is toLex fun n => n == 1 but your algorithm gives toLex fun n => n == 0 && n == 1

[Violeta Hernández]

hm you're right it's clearly a bit more subtle than that

[Aaron Liu]

just do what I did

[Violeta Hernández]

Ok yeah you know what I'm starting to think this is actually one of those cases where you need to use ordinal induction

[Violeta Hernández]

Aaron Liu said:

just do what I did

I admit I haven't quite figured out what you did

[Violeta Hernández]

Ok fine, I'm now convinced that building the complete lattice structure on lexicographically ordered functions requires ordinal induction

[Aaron Liu]

Violeta Hernández said:

Ok fine, I'm now convinced that building the complete lattice structure on lexicographically ordered functions requires ordinal induction

There is a way to avoid it

[Violeta Hernández]

the plot thickens

[Aaron Liu]

Basically you do well founded induction on LT instead

[Violeta Hernández]

well i mean yeah