Commit 2023-09-27 08:12 aa7c8c33

View on Github →

feat: Embed a gen. Bool. alg. into a Bool. alg. (#7371) This is useful to prove that Boolean algebra results not mentioning compl and top also hold in generalised Boolean algebras.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Booleanisation.lean

added def Booleanisation.comp

added theorem Booleanisation.comp_bot

added theorem Booleanisation.comp_inf_comp

added theorem Booleanisation.comp_inf_lift

added theorem Booleanisation.comp_le_comp

added theorem Booleanisation.comp_lt_comp

added theorem Booleanisation.comp_sdiff_comp

added theorem Booleanisation.comp_sdiff_lift

added theorem Booleanisation.comp_sup_comp

added theorem Booleanisation.comp_sup_lift

added theorem Booleanisation.compl_comp

added theorem Booleanisation.compl_lift

added def Booleanisation.lift

added def Booleanisation.liftLatticeHom

added theorem Booleanisation.liftLatticeHom_injective

added theorem Booleanisation.lift_bot

added theorem Booleanisation.lift_inf_comp

added theorem Booleanisation.lift_inf_lift

added theorem Booleanisation.lift_le_comp

added theorem Booleanisation.lift_le_lift

added theorem Booleanisation.lift_lt_comp

added theorem Booleanisation.lift_lt_lift

added theorem Booleanisation.lift_sdiff_comp

added theorem Booleanisation.lift_sdiff_lift

added theorem Booleanisation.lift_sup_comp

added theorem Booleanisation.lift_sup_lift

added theorem Booleanisation.not_comp_le_lift

added theorem Booleanisation.not_comp_lt_lift

added def Booleanisation