a < b and b < a -> false

Stream: Is there code for X?

[Henrik Böving]

Do we have:

import Mathlib.Order.Defs.PartialOrder

example (a b : β) [Preorder β] (h1 : a < b) (h2 : b < a) : False :=
  lt_irrefl _ (lt_trans h1 h2)

somewhere?

[Henrik Böving]

not_lt_of_gt is a variation i guess

[Edward van de Meent]

docs#lt_asymm

[Henrik Böving]

https://loogle.lean-lang.org/?q=%7C-+%3Fx+%3C+%3Fy+%E2%86%92+%3Fy+%3C+%3Fx+%E2%86%92+False why did my loogle query not find those :(

[Kevin Buzzard]

https://loogle.lean-lang.org/?q=%7C-+%3Fx+%3C+%3Fy+%E2%86%92+%C2%AC+%28%3Fy+%3C+%3Fx%29 works, so maybe loogle doesn't see through \not P = P \to False

[Henrik Böving]

@Joachim Breitner pretty please? :P

[Daniel Weber]

I think the problem isn't that, but that it looks for definitions mentioning False, while the definition actually mentions Not instead

[Daniel Weber]

Perhaps that could be resolved by unfolding reducible definitions before doing that search

[Joachim Breitner]

The handling of reducible definitions in loogle is incomplete, if not buggy. When I wrote loogle I didn't really understand all this well (and knew I didn’t), so I postponed this. Now that I understand it a big better I should revise this (probably by unfolding reducible definitions before indexing and before searching). Although I’m surprised this doesn't cause confusion more often.

[Joachim Breitner]

Although as a user looking for the symmetric lemma that Henrik searched, I am not sure I find docs#lt_asymm satisfying. I guess it works well if you really internalized negation as P → False, but otherwise it might be nicer to have the → False lemmas as well?

[Eric Wieser]

I think this is consistent with docs#IsAsymm which seems to be about the reverse relation not holding, rather than about the pair of relations being contradictory