archimedean): Comparing with rationals determines the order (#13602)

Commit

3 years ago

feat(algebra/order/archimedean): Comparing with rationals determines the order (#13602) In a linear ordered field, if `q < x → q ≤ y` for all `q : ℚ`, then `x ≤ y`, and similar results.

Author

YaelDillies

Parents

b98bd418

mathlib3 976c544c - feat(algebra/order/archimedean): Comparing with rationals determines the order (#13602)

mathlib3
976c544c - feat(algebra/order/archimedean): Comparing with rationals determines the order (#13602)