Commit 2022-12-29 11:06 b291d234

View on Github →

feat: port Order.ModularLattice (#1234)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/ModularLattice.lean

added theorem Disjoint.disjoint_sup_left_of_disjoint_sup_right

added theorem Disjoint.disjoint_sup_right_of_disjoint_sup_left

added def IsCompl.iicOrderIsoIci

added theorem IsModularLattice.inf_sup_inf_assoc

added theorem IsModularLattice.sup_inf_sup_assoc

added theorem covby_sup_of_inf_covby_left

added theorem covby_sup_of_inf_covby_of_inf_covby_left

added theorem covby_sup_of_inf_covby_of_inf_covby_right

added theorem covby_sup_of_inf_covby_right

added theorem eq_of_le_of_inf_le_of_sup_le

added def infIccOrderIsoIccSup

added def infIooOrderIsoIooSup

added theorem inf_covby_of_covby_sup_left

added theorem inf_covby_of_covby_sup_of_covby_sup_left

added theorem inf_covby_of_covby_sup_of_covby_sup_right

added theorem inf_covby_of_covby_sup_right

added theorem inf_lt_inf_of_lt_of_sup_le_sup

added theorem inf_strictMonoOn_Icc_sup

added theorem inf_sup_assoc_of_le

added theorem isModularLattice_iff_inf_sup_inf_assoc

added theorem sup_inf_assoc_of_le

added theorem sup_lt_sup_of_lt_of_inf_le_inf

added theorem sup_strictMonoOn_Icc_inf

added theorem wellFounded_gt_exact_sequence

added theorem wellFounded_lt_exact_sequence