Are cauchy sequences a partial order?

Stream: mathlib4

[Alex Meiburg]

Given a [LinearOrderedField α], there is no instance of PartialOrder (CauSeq α abs) that mathlib is currently able to synthesize. Is this (1) a natural thing that should be in mathlib but just no one has written it yet; (2) in mathlib but I'm doing something wrong that's stopping it from getting synthesized; (3) actually mathematically incorrect somehow?

Because I certainly _think_ of cauchy sequences as forming a partial order, indeed I think of the reals that way, but maybe that somehow involves an aspect unique to ℚ that doesn't hold in general.

(I actually wanted CauSeq to be a Lattice, so that I could use docs#neg_inf , but there wasn't even PartialOrder.)

[Alex Meiburg]

Oh, I see the issue now. PartialOrder requires "∀ a b : α, a ≤ b → b ≤ a → a = b", but with CauSeq you can only conclude ≈. Equality is actually elementwise equality.

[Alex Meiburg]

Real is the quotient of CauSeq by it's natural equivalence, specifically on the rationals. Because you actually get = instead of ≈, it is (usually) much cleaner to work with. Is there no generic "quotient of CauSeq" that works for any LinearOrderedField? In other words, why is Real defined as the quotient over rationals, instead of some "CauSeqEquiv" (with most of the nice properties) over the rationals?

[Yaël Dillies]

Do you know that docs#CauSeq is a pretty hands on construction of the reals and that more general theory is available when looking at docs#CauchyFilter ?

[Alex Meiburg]

I did not! Thanks for the pointer. Also, that looks like it's far off in pointset topology land where I dare not venture, but I will take a look anyway :)

[Matt Diamond]

keep in mind that there are lemmas like docs#Metric.cauchySeq_iff that allow you to translate between different characterizations, some of which may be more familiar

[Matt Diamond]

(and docs#isCauSeq_iff_cauchySeq proves that the two constructions are equivalent in a normed field)