Metamath Proof Explorer
Table of Contents - 20.3.8. Extensible Structures
- Structure restriction operator
- ressplusf
- ressnm
- abvpropd2
- The opposite group
- oppgle
- oppgleOLD
- oppglt
- Posets
- ressprs
- oduprs
- posrasymb
- resspos
- resstos
- odutos
- tlt2
- tlt3
- trleile
- toslublem
- toslub
- tosglblem
- tosglb
- Complete lattices
- clatp0cl
- clatp1cl
- Order Theory
- cmnt
- cmgc
- df-mnt
- df-mgc
- mntoval
- ismnt
- ismntd
- mntf
- mgcoval
- mgcval
- mgcf1
- mgcf2
- mgccole1
- mgccole2
- mgcmnt1
- mgcmnt2
- mgcmntco
- dfmgc2lem
- dfmgc2
- mgcmnt1d
- mgcmnt2d
- mgccnv
- pwrssmgc
- mgcf1olem1
- mgcf1olem2
- mgcf1o
- Extended reals Structure - misc additions
- ax-xrssca
- ax-xrsvsca
- xrs0
- xrslt
- xrsinvgval
- xrsmulgzz
- xrstos
- xrsclat
- xrsp0
- xrsp1
- ressmulgnn
- ressmulgnn0
- The extended nonnegative real numbers commutative monoid
- xrge0base
- xrge00
- xrge0plusg
- xrge0le
- xrge0mulgnn0
- xrge0addass
- xrge0addgt0
- xrge0adddir
- xrge0adddi
- xrge0npcan
- fsumrp0cl