Lean4
instance instSemilatticeInf : SemilatticeInf (Booleanisation α)
where
inf x y := min x y
inf_le_left
| lift a, lift b => LE.lift inf_le_left
| lift a, comp b => LE.lift sdiff_le
| comp a, lift b => LE.sep disjoint_sdiff_self_left
| comp a, comp b => LE.comp le_sup_left
inf_le_right
| lift a, lift b => LE.lift inf_le_right
| lift a, comp b => LE.sep disjoint_sdiff_self_left
| comp a, lift b => LE.lift sdiff_le
| comp a, comp b => LE.comp le_sup_right
le_inf
| lift a, lift b, lift c, LE.lift hab, LE.lift hac => LE.lift <| le_inf hab hac
| lift a, lift b, comp c, LE.lift hab, LE.sep hac => LE.lift <| le_sdiff.2 ⟨hab, hac⟩
| lift a, comp b, lift c, LE.sep hab, LE.lift hac => LE.lift <| le_sdiff.2 ⟨hac, hab⟩
| lift a, comp b, comp c, LE.sep hab, LE.sep hac => LE.sep <| hab.sup_right hac
| comp a, comp b, comp c, LE.comp hba, LE.comp hca => LE.comp <| sup_le hba hca
