Commit 2024-01-26 19:09 f1802b11

View on Github →

feat: Add lattice lemmas about Sub{group,monoid}.{op,unop} (#9860) In fact I only need the closure lemma, but the others are easy enough. This changes the opEquivs to be order isomorphisms rather than just Equivs.

Estimated changes

added theorem Subgroup.le_op_iff
added theorem Subgroup.mem_op
added theorem Subgroup.mem_unop
modified def Subgroup.opEquiv
added theorem Subgroup.op_bot
added theorem Subgroup.op_closure
added theorem Subgroup.op_iInf
added theorem Subgroup.op_iSup
added theorem Subgroup.op_inf
added theorem Subgroup.op_le_iff
added theorem Subgroup.op_le_op_iff
added theorem Subgroup.op_sInf
added theorem Subgroup.op_sSup
added theorem Subgroup.op_sup
modified theorem Subgroup.op_toSubmonoid
added theorem Subgroup.op_top
added theorem Subgroup.op_unop
added theorem Subgroup.unop_bot
added theorem Subgroup.unop_closure
added theorem Subgroup.unop_iInf
added theorem Subgroup.unop_iSup
added theorem Subgroup.unop_inf
added theorem Subgroup.unop_op
added theorem Subgroup.unop_sInf
added theorem Subgroup.unop_sSup
added theorem Subgroup.unop_sup
modified theorem Subgroup.unop_toSubmonoid
added theorem Subgroup.unop_top
added theorem Submonoid.le_op_iff
added theorem Submonoid.mem_op
added theorem Submonoid.mem_unop
modified def Submonoid.opEquiv
added theorem Submonoid.op_bot
added theorem Submonoid.op_closure
added theorem Submonoid.op_iInf
added theorem Submonoid.op_iSup
added theorem Submonoid.op_inf
added theorem Submonoid.op_le_iff
added theorem Submonoid.op_le_op_iff
added theorem Submonoid.op_sInf
added theorem Submonoid.op_sSup
added theorem Submonoid.op_sup
added theorem Submonoid.op_top
added theorem Submonoid.op_unop
added theorem Submonoid.unop_bot
added theorem Submonoid.unop_closure
added theorem Submonoid.unop_iInf
added theorem Submonoid.unop_iSup
added theorem Submonoid.unop_inf
added theorem Submonoid.unop_op
added theorem Submonoid.unop_sInf
added theorem Submonoid.unop_sSup
added theorem Submonoid.unop_sup
added theorem Submonoid.unop_top