Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-14 05:27 b8858394

View on Github →

refactor(data/set/intervals): Generalize set.interval to lattices (#17776) Replace

def interval (a b : α) := Icc (min a b) (max a b)

by

def interval (a b : α) := Icc (a ⊓ b) (a ⊔ b)

Generalize lemmas accordingly.

Estimated changes

added theorem set.Icc_min_max
modified theorem set.Icc_subset_interval'
modified theorem set.Icc_subset_interval
modified def set.interval
modified theorem set.interval_of_not_ge
modified theorem set.interval_of_not_le
modified theorem set.interval_self
modified theorem set.interval_swap
modified theorem set.left_mem_interval
modified theorem set.mem_interval_of_ge
modified theorem set.mem_interval_of_le
modified theorem set.nonempty_interval
modified theorem set.right_mem_interval