Metamath Proof Explorer

Table of Contents - 19.7. States on a Hilbert lattice and Godowski's equation

1. States on a Hilbert lattice
   1. df-st
   2. df-hst
   3. isst
   4. ishst
   5. sticl
   6. stcl
   7. hstcl
   8. hst1a
   9. hstel2
   10. hstorth
   11. hstosum
   12. hstoc
   13. hstnmoc
   14. stge0
   15. stle1
   16. hstle1
   17. hst1h
   18. hst0h
   19. hstpyth
   20. hstle
   21. hstles
   22. hstoh
   23. hst0
   24. sthil
   25. stj
   26. sto1i
   27. sto2i
   28. stge1i
   29. stle0i
   30. stlei
   31. stlesi
   32. stji1i
   33. stm1i
   34. stm1ri
   35. stm1addi
   36. staddi
   37. stm1add3i
   38. stadd3i
   39. st0
   40. strlem1
   41. strlem2
   42. strlem3a
   43. strlem3
   44. strlem4
   45. strlem5
   46. strlem6
   47. stri
   48. strb
   49. hstrlem2
   50. hstrlem3a
   51. hstrlem3
   52. hstrlem4
   53. hstrlem5
   54. hstrlem6
   55. hstri
   56. hstrbi
   57. largei
   58. jplem1
   59. jplem2
   60. jpi
2. Godowski's equation
   1. golem1
   2. golem2
   3. goeqi
   4. stcltr1i
   5. stcltr2i
   6. stcltrlem1
   7. stcltrlem2
   8. stcltrthi