Zulip Chat Archive

Stream: Is there code for X?

Topic: completion of boolean algebra


view this post on Zulip Kenny Lau (Dec 13 2020 at 07:51):

The completion of a docs#boolean_algebra is an embedding to a docs#complete_boolean_algebra with dense image. Do we have it in mathlib?

view this post on Zulip 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

view this post on Zulip Adam Topaz (Dec 13 2020 at 14:24):

Flypitch might have something. Doesn't this come up in forcing?

view this post on Zulip 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