How to write this statement regarding partial orders

Stream: mathlib4

[The-Anh Vu-Le]

I want to say "there does not exist a partial order on \N such that ...". However, writing ¬ ∃ R : PartialOrder ℕ, P(R) seems like a bad idea (apparently it will refer to the already defined partial order \le on \N). How do I write it better?

To give more details, I am trying to prove that "there does not exist a partial order R on \N such that B is a subset of R" (where B is a specific set, but the definition does not matter here). What I have tried is

¬ ∃ R : PartialOrder ℕ, ∀ p ∈ B, R.le p.1 p.2

which is not a good idea as stated above.

[Walter Moreira]

Instead of quantifying over the class PartialOrder, perhaps it could be useful to use IsPartialOrder:

import Mathlib

example (P : (ℕ → ℕ → Prop) → Prop) :
  ¬ ∃ (r : ℕ → ℕ → Prop), IsPartialOrder ℕ r ∧ P r := by sorry

I didn't try to actually prove anything with that, but the order in this formulation is an arbitrary order, not just the usual order in Nat. (Disclaimer, I'm a beginner in Lean, there might be a more proper expression for your issue. Hope it helps...)

[The-Anh Vu-Le]

I did not realize there is a IsPartialOrder class. Thanks!

[Walter Moreira]

Just a follow up: looking at the use of IsPartialOrder and similar classes in Mathlib, what I wrote before seems non-standard. In Mathlib it is always used as an argument [IsPartialOrder Nat r], instead of as a predicate. Please, be careful not going into a rabbit hole from my suggestion.

[The-Anh Vu-Le]

I don't think it is wrong, though. I have completed the proof with it.

[Walter Moreira]

You are right, there are some statements that use it in that way. For example docs#extend_partialOrder. Glad it helped.

[Josha Dekker]

An alternative way of writing the claim in the original post is to say “if I have a partial order on N, P fails”, this is also a way in which you may write the result

[Violeta Hernández]

I would generally avoid IsPartialOrder. Some of these unbundled classes do see a lot of use, particularly the ones for relations that are one of reflexive/antisymmetric/transitive, but if you have all of these properties then you likely also want to talk about the < relation which is very awkward to do with this unbundled approach.

[Violeta Hernández]

But if it works it works, I guess.