Lean4
instance instSemilatticeSup : SemilatticeSup (Booleanisation α)
where
sup x y := max x y
le_sup_left
| lift a, lift b => LE.lift le_sup_left
| lift a, comp b => LE.sep disjoint_sdiff_self_right
| comp a, lift b => LE.comp sdiff_le
| comp a, comp b => LE.comp inf_le_left
le_sup_right
| lift a, lift b => LE.lift le_sup_right
| lift a, comp b => LE.comp sdiff_le
| comp a, lift b => LE.sep disjoint_sdiff_self_right
| comp a, comp b => LE.comp inf_le_right
sup_le
| lift a, lift b, lift c, LE.lift hac, LE.lift hbc => LE.lift <| sup_le hac hbc
| lift a, lift b, comp c, LE.sep hac, LE.sep hbc => LE.sep <| hac.sup_left hbc
| lift a, comp b, comp c, LE.sep hac, LE.comp hcb => LE.comp <| le_sdiff.2 ⟨hcb, hac.symm⟩
| comp a, lift b, comp c, LE.comp hca, LE.sep hbc => LE.comp <| le_sdiff.2 ⟨hca, hbc.symm⟩
| comp a, comp b, comp c, LE.comp hca, LE.comp hcb => LE.comp <| le_inf hca hcb
