Zulip Chat Archive

Stream: new members

Topic: placing a lemma about partial orders


view this post on Zulip Yakov Pechersky (Jan 14 2021 at 02:12):

Where in mathlib would this go, if anywhere?

@[simp] lemma ne_iff_lt_iff_le {α : Type*} [partial_order α] {n m : α} : (n  m  n < m)  n  m :=
begin
  refine λ h, _, λ h, _⟩,
  { by_cases H : n = m,
    { exact le_of_eq H },
    { exact le_of_lt (h.mp H) } },
  { rcases eq_or_lt_of_le h with rfl|H,
    { simp [not_lt_of_ge] },
    { simp [H, ne_of_lt] } }
end

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 02:12):

And why is not_lt_of_ge true for partial_order but le_of_not_gt needs linear_order?

view this post on Zulip Mario Carneiro (Jan 14 2021 at 02:53):

(1) Somewhere in algebra.order; (2) because le_of_not_gt has the form not A -> B, which is a disjunction A \/ B, and disjunctions like this usually only hold in the total order case

view this post on Zulip Mario Carneiro (Jan 14 2021 at 02:55):

The other direction A -> not B is closer to asymmetry, which has the form A -> B -> false and is true in any preorder

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 02:56):

Gotcha. Issue was that \not k < k was not simplifying for a partial_order in a lemma that I have.

view this post on Zulip Mario Carneiro (Jan 14 2021 at 03:00):

that's lt_irrefl

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 03:02):

Hmm why did I think that required linear_order? Must've gotten some wires crossed.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 03:17):

#5731


Last updated: May 08 2021 at 18:17 UTC