## Stream: Is there code for X?

### Topic: Distrib lattice constructors

#### 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?

#### Yury G. Kudryashov (Aug 03 2020 at 05:44):

Is it the same as order_dual.distrib_lattice?

#### 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 }.

#### 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