Ioo_inter_Ioi

Stream: Is there code for X?

[Jireh Loreaux]

Are we really missing this one? I couldn't find it (or the LinearOrder variant with max)

import Mathlib

lemma Set.Ioo_inter_Ioi_of_le {α : Type*} [Preorder α] {a b c : α} (h : a ≤ c) :
    Set.Ioo a b ∩ Set.Ioi c = Set.Ioo c b := by
  ext x
  simp only [mem_inter_iff, mem_Ioo, mem_Ioi, and_comm (a := c < x), and_congr_left_iff,
    and_iff_right_iff_imp]
  exact fun hc _ ↦ h.trans_lt hc

[Anatole Dedecker]

I can't find it, but here's a golf:

import Mathlib

lemma Set.Ioo_inter_Ioi_of_le {α : Type*} [Preorder α] {a b c : α} (h : a ≤ c) :
    Set.Ioo a b ∩ Set.Ioi c = Set.Ioo c b := by
  rw [← Ioi_inter_Iio, ← Ioi_inter_Iio, inter_comm, ← inter_assoc,
      inter_eq_left.mpr (Ioi_subset_Ioi h)]