Zulip Chat Archive

Stream: general

Topic: Obvious gap

Yaël Dillies (Jan 27 2022 at 07:29):

In the category of "How come we not have that", I just found that mathlib doesn't know docs#bool is a docs#boolean_algebra. It actually even is a docs#complete_boolean_algebra.

Kevin Buzzard (Jan 27 2022 at 09:23):

Last time I looked we didn't have => for bool (ff => tt is tt, tt => ff is ff etc).

Kevin Buzzard (Jan 27 2022 at 09:23):

Underlines how bool isn't used for reasoning

Yaël Dillies (Jan 27 2022 at 09:25):

It will soon be! Monotone maps to bool form the Janusian object of the equivalence of categories between FinDistribLattice and FinPartialOrder. cf #11677

Last updated: Dec 20 2023 at 11:08 UTC