Commit 2024-01-16 16:52 18eeff5e

View on Github →

refactor: Clean up posPart (#9740) This changes the typeclass notation approach with plain functions. Followup to #9553. Part of #9411

Estimated changes

added theorem inv_le_leOnePart
added def leOnePart
added theorem leOnePart_anti
added theorem leOnePart_eq_inv'
added theorem leOnePart_eq_inv
added theorem leOnePart_eq_one'
added theorem leOnePart_eq_one
added theorem leOnePart_inv
added theorem leOnePart_le_one'
added theorem leOnePart_le_one
added theorem leOnePart_one
added theorem le_oneLePart
added def oneLePart
added theorem oneLePart_eq_one
added theorem oneLePart_eq_self
added theorem oneLePart_inv
added theorem oneLePart_le_one
added theorem oneLePart_mono
added theorem oneLePart_one
added theorem one_le_leOnePart
added theorem one_le_oneLePart
deleted theorem continuous_neg'
added theorem continuous_negPart
deleted theorem continuous_pos
added theorem continuous_posPart
modified theorem isClosed_nonneg
added theorem lipschitzWith_negPart
deleted theorem lipschitzWith_pos
added theorem lipschitzWith_posPart