Intervals in with_top α
and with_bot α
#
In this file we prove various lemmas about set.image
s and set.preimage
s of intervals under
coe : α → with_top α
and coe : α → with_bot α
.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]