Commit 2023-04-10 11:19 74e4a559

View on Github →

feat: port Order.Height (#2186)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.some_eq_coe

Modified Mathlib/Data/ENat/Lattice.lean

added theorem ENat.coe_supᵢ

added theorem ENat.supᵢ_coe_lt_top

Created Mathlib/Order/Height.lean

added theorem Set.chainHeight_add_le_chainHeight_add

added theorem Set.chainHeight_dual

added theorem Set.chainHeight_empty

added theorem Set.chainHeight_eq_supᵢ_Ici

added theorem Set.chainHeight_eq_supᵢ_Iic

added theorem Set.chainHeight_eq_supᵢ_subtype

added theorem Set.chainHeight_eq_top_iff

added theorem Set.chainHeight_eq_zero_iff

added theorem Set.chainHeight_image

added theorem Set.chainHeight_insert_of_forall_gt

added theorem Set.chainHeight_insert_of_forall_lt

added theorem Set.chainHeight_le_chainHeight_TFAE

added theorem Set.chainHeight_le_chainHeight_iff

added theorem Set.chainHeight_le_chainHeight_iff_le

added theorem Set.chainHeight_mono

added theorem Set.chainHeight_of_isEmpty

added theorem Set.chainHeight_union_eq

added theorem Set.chainHeight_union_le

added theorem Set.cons_mem_subchain_iff

added theorem Set.exists_chain_of_le_chainHeight

added theorem Set.le_chainHeight_TFAE

added theorem Set.le_chainHeight_add_nat_iff

added theorem Set.le_chainHeight_iff

added theorem Set.length_le_chainHeight_of_mem_subchain

added theorem Set.nil_mem_subchain

added theorem Set.one_le_chainHeight_iff

added theorem Set.singleton_mem_subchain_iff

added def Set.subchain

added theorem Set.wellFoundedGT_of_chainHeight_ne_top

added theorem Set.wellFoundedLT_of_chainHeight_ne_top