2025.07.18
https://gyazo.com/898ae284260e837602acb721574efd30
前：
2025.07.17
後：
2025.07.19
#日報
メモ
近傍フレームがカノニカルであるというのはフレームの
$ W
が
極大無矛盾集合
全体になっていればよい，というのが条件になっているのだが，これをLeanで素朴にやると代入操作がグチャグチャになって面倒．
なのだがどうすればいいのかはよくわかｒなない．
思った
いよいよ明日が
RealSample
です