## Stream: new members

### Topic: placing a lemma about partial orders

#### 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


#### 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?

#### 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

#### 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

#### 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.

#### Mario Carneiro (Jan 14 2021 at 03:00):

that's lt_irrefl

#### Yakov Pechersky (Jan 14 2021 at 03:02):

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

#### Yakov Pechersky (Jan 14 2021 at 03:17):

#5731

Last updated: May 08 2021 at 18:17 UTC