Zulip Chat Archive

Stream: Is there code for X?

Topic: not_mem lemmas


view this post on Zulip Benjamin Davidson (Feb 14 2021 at 10:00):

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

view this post on Zulip Eric Wieser (Feb 14 2021 at 10:16):

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

view this post on Zulip Benjamin Davidson (Feb 15 2021 at 01:25):

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

view this post on Zulip Benjamin Davidson (Feb 15 2021 at 06:55):

#6238


Last updated: May 16 2021 at 05:21 UTC