Commit 2023-05-22 16:35 02858e21

View on Github →

feat: port Order.Interval (#3360)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Interval.lean

added theorem Interval.bot_ne_pure

added def Interval.coeHom

added theorem Interval.coe_bot

added theorem Interval.coe_coe

added theorem Interval.coe_dual

added theorem Interval.coe_iInf

added theorem Interval.coe_iInf₂

added theorem Interval.coe_inf

added theorem Interval.coe_inj

added theorem Interval.coe_injective

added theorem Interval.coe_pure

added theorem Interval.coe_sInf

added theorem Interval.coe_sSubset_coe

added theorem Interval.coe_subset_coe

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 theorem Interval.mem_pure

added theorem Interval.mem_pure_self

added def Interval.pure

added theorem Interval.pure_injective

added theorem Interval.pure_ne_bot

added theorem Interval.subset_coe_map

added theorem Interval.«exists»

added theorem Interval.«forall»

added def Interval

added def NonemptyInterval.coeHom

added theorem NonemptyInterval.coe_coeHom

added theorem NonemptyInterval.coe_dual

added theorem NonemptyInterval.coe_eq_pure

added theorem NonemptyInterval.coe_nonempty

added theorem NonemptyInterval.coe_pure

added theorem NonemptyInterval.coe_pure_interval

added theorem NonemptyInterval.coe_ssubset_coe

added theorem NonemptyInterval.coe_subset_coe

added theorem NonemptyInterval.coe_sup_interval

added theorem NonemptyInterval.coe_top

added theorem NonemptyInterval.coe_top_interval

added def NonemptyInterval.dual

added theorem NonemptyInterval.dual_map

added theorem NonemptyInterval.dual_map₂

added theorem NonemptyInterval.dual_pure

added theorem NonemptyInterval.dual_top

added theorem NonemptyInterval.ext

added theorem NonemptyInterval.ext_iff

added theorem NonemptyInterval.fst_dual

added theorem NonemptyInterval.fst_sup

added theorem NonemptyInterval.le_def

added def NonemptyInterval.map

added theorem NonemptyInterval.map_map

added theorem NonemptyInterval.map_pure

added def NonemptyInterval.map₂

added theorem NonemptyInterval.map₂_pure

added theorem NonemptyInterval.mem_coe_interval

added theorem NonemptyInterval.mem_def

added theorem NonemptyInterval.mem_mk

added theorem NonemptyInterval.mem_pure

added theorem NonemptyInterval.mem_pure_self

added def NonemptyInterval.pure

added theorem NonemptyInterval.pure_injective

added theorem NonemptyInterval.snd_dual

added theorem NonemptyInterval.snd_sup

added theorem NonemptyInterval.subset_coe_map

added def NonemptyInterval.toDualProd

added def NonemptyInterval.toDualProdHom

added theorem NonemptyInterval.toDualProd_apply

added theorem NonemptyInterval.toDualProd_injective

added theorem NonemptyInterval.toProd_injective

added structure NonemptyInterval

Modified Mathlib/Order/WithBot.lean