unordered intervals

Stream: general

[Yury G. Kudryashov]

Should we have something more generic for unordered intervals? We already have unordered Icc and Ioc intervals. Several theorems like docs#complex.integral_boundary_rect_eq_zero_of_continuous_on_of_differentiable_on use unordered Ioo intervals (and it looks ugly without a definition). Should we have something like this?

def set.unordered_Ixx {α : Type*} [linear_order α] (Ixx : α → α → set α) (a b : α) : set α :=
Ixx (min a b) (max a b)

notation `ICC` := unordered_Ixx Icc
notation `IOC` := unordered_Ixx Ioc
notation `ICO` := unordered_Ixx Ico
notation `IOO` := unordered_Ixx Ioo

[Yury G. Kudryashov]

Discussion about long names in that file moved to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lemma.20names.20in.20cauchy_integral.2Elean

[Yaël Dillies]

Same thought here, except that you shouldn't use one def + notation but directly call the defs set.IXX (for when we'll want the finset versions)

[Yury G. Kudryashov]

If we use definitions, then we'll need to repeat some theorems three or for times. I'm not sure if this is really bad. I'll think again in the morning.

[Yaël Dillies]

We already do this for set.Ixx (and actually 8 times if you take finset.Ixx into account!), so that seems like the natural continuation, unless you want IXX to be a really thin wrapper around Ixx and always walk up to Ixx in proofs involving IXX.

[Kevin Buzzard]

I never understand why people object to code reuse. Argument reuse happens across mathematics and sometimes it really is the case that there"s no underlying theorem which is the root cause -- it's a more abstract "principle" which refuses to be boxed into a concrete abstraction. Martin Hairer once emphasised this to me in a conversation we had about formalising his area.

[Yury G. Kudryashov]

There is a trade-off here: code reuse vs discoverability of lemmas. In case of generic defs and lemmas, they will be named unordered_symm/unordered_of_le or IXX_symm/IXX_of_le instead of ICC_symm/ICC_of_le.