Mathlib v3 is deprecated. Go to Mathlib v4

Def distrib_lattice.of_inf_sup_le

Modification history

2022-07-15 01:25
src/order/lattice.lean
feat(order/complete_boolean_algebra): A frame is distributive (#15340) …
Added distrib_lattice.of_inf_sup_leView on Github →