Commit 2024-10-08 14:03 f3bcc3bb

View on Github →

docs: add latex doc for Set and Finset intervals (#17523) Add LaTeX descriptions for all Icc/Ico/Ioc/Ioo/Iio/Ioi/Iic/Ici intervals. Following this zulip thread.

Estimated changes

Modified Mathlib/Order/Interval/Finset/Defs.lean

modified def Finset.Iic

modified def Finset.Iio

Modified Mathlib/Order/Interval/Set/Basic.lean

modified def Set.Iio