not_mem lemmas

Stream: Is there code for X?

[Benjamin Davidson]

Do there already exist lemmas for the following? (Or for other sets?)

import data.set.intervals.unordered_interval
import data.real.basic

open real set

lemma not_mem_interval_of_lt {a b c : ℝ} (ha : c < a) (hb : c < b) : c ∉ interval a b :=
begin
  simp only [interval, not_and, min_le_iff, le_max_iff, mem_Icc, not_or_distrib],
  rw [← not_lt, ← not_lt, ← not_and_distrib],
  intro hnot,
  by_contra,
  exact not_and.mp hnot ha hb,
end

lemma not_mem_interval_of_gt {a b c : ℝ} (ha : a < c) (hb : b < c) : c ∉ interval a b :=
begin
  simp only [interval, not_and, min_le_iff, le_max_iff, mem_Icc, not_or_distrib, not_le],
  exact λ h, ⟨ha, hb⟩,
end

[Eric Wieser]

How different is docs#set.interval to docs#set.Icc? (Ah, the former is agnostic to the order of the bounds)

[Benjamin Davidson]

It seems like these don't exist so I will add them for the various different sets.

[Benjamin Davidson]

#6238