Zulip Chat Archive

Stream: Is there code for X?

Topic: Distrib lattice constructors


view this post on Zulip Bhavik Mehta (Aug 02 2020 at 13:27):

Is there a constructor for distrib_lattice using this distributive law:
x ⊓ (y ⊔ z) ≤ (x ⊓ y) ⊔ (x ⊓ z) instead of the one given there - it's mentioned that they're equivalent but only one is provided seemingly?

view this post on Zulip Yury G. Kudryashov (Aug 03 2020 at 05:44):

Is it the same as order_dual.distrib_lattice?

view this post on Zulip Yury G. Kudryashov (Aug 03 2020 at 05:46):

I mean, there is no constructor using this law now but probably you can write something like letI : distrib_lattice (order_dual α) := { .. order_dual.lattice, your_lemma }; exact { sup := ...; (other operations); .. show distrib_lattice (order_dual $ order_dual α), by apply_instance }.

view this post on Zulip Yury G. Kudryashov (Aug 03 2020 at 05:46):

Though possibly a better approach is to prove some iff or tfae for a lattice.


Last updated: May 07 2021 at 22:14 UTC