Intersection of intervals

Stream: new members

[Iocta]

Is there a theorem that the intersection of two intervals is an interval, likeinter (Icc a b) (Icc c d) = Icc a d and likewise with Ioo Ioc , etc?

[Iocta]

theorem Ioo_inter_Ioo (la ra lb rb : ℝ) :
  Set.Ioo la ra ∩ Set.Ioo lb rb = Set.Ioo (la ⊓ lb) (ra ⊔ rb) := by
  apply Set.ext
  intro x
  simp
  apply Iff.intro
  {
    intro h
    let ⟨⟨hal, har⟩, ⟨hbl, hbr⟩⟩ := h
    simp_all
  }
  {
    intro h
    let ⟨hl, hr⟩ := h
    apply And.intro
    { simp_all only [and_self] }
    { simp_all only [and_self] }
  }

[Iocta]

There are 16 of these and they all have identical proofs. There must be a way to handle this situation.

[Eric Wieser]

docs#Set.Ioo_inter_Ioo interestingly says something different!

[Eric Wieser]

Oh, your proof is incompelte!

[Eric Wieser]

There is an error on the }s

[Iocta]

oops , yeah swapped the operators

[Iocta]

UI didn't make it very easy to notice - just one squiggly underneath the }

[Iocta]

How come there's no Icc_inter_Ioo?

[Philippe Duchon]

You cannot know whether the intersection of a closed interval and an open one will be open or closed (either on the left or the right) if you don't have a hypothesis on the corresponding interval bounds, this is my guess.