Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-07 09:54 63014d26

View on Github →

feat(order/interval): Order intervals (#14807) Define nonempty_interval, the type of nonempty intervals in an order, namely pairs where the second element is greater than the first, and interval α as with_bot (nonempty_interval α).

Estimated changes

added theorem option.map_comm
added theorem with_bot.coe_inj
added theorem with_bot.coe_injective
added theorem with_bot.map_comm
added theorem with_top.map_comm
added theorem interval.coe_Inf
added theorem interval.coe_bot
added theorem interval.coe_coe
added theorem interval.coe_dual
added def interval.coe_hom
added theorem interval.coe_inf
added theorem interval.coe_infi
added theorem interval.coe_infi₂
added theorem interval.coe_inj
added theorem interval.coe_injective
added theorem interval.coe_pure
added theorem interval.coe_top
added theorem interval.disjoint_coe
added def interval.dual
added theorem interval.dual_bot
added theorem interval.dual_map
added theorem interval.dual_pure
added theorem interval.dual_top
added def interval.map
added theorem interval.map_map
added theorem interval.map_pure
added def interval.pure
added theorem interval.«exists»
added theorem interval.«forall»
added def interval
added structure nonempty_interval