Commit 2024-08-05 08:52 f74b424c

View on Github →

feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas (#15271)

Estimated changes

added theorem ciInf_image
added theorem ciInf_subtype''
added theorem ciInf_subtype'
added theorem ciInf_subtype
added theorem ciSup_image
added theorem ciSup_or'
added theorem ciSup_subtype''
added theorem ciSup_subtype'
added theorem ciSup_subtype
added theorem csInf_image
added theorem csSup_image