Stream: Is there code for X?
Kenny Lau (Dec 13 2020 at 07:51):
Adam Topaz (Dec 13 2020 at 14:22):
I would be surprised. Last time I checked I didn't even find morphisms of boolean algebras in mathlib
Adam Topaz (Dec 13 2020 at 14:24):
Flypitch might have something. Doesn't this come up in forcing?
Jesse Michael Han (Dec 13 2020 at 15:59):
we end up showing certain forcing posets are dense in certain boolean algebras but there's not a substantial API around the notion of completion/dense embedding
Last updated: May 16 2021 at 05:21 UTC