instDistribLattice — Mathlib

Lean4
instance instDistribLattice : DistribLattice (Booleanisation α)
    where
  inf x y := x ⊓ y
  inf_le_left _ _ := inf_le_left
  inf_le_right _ _ := inf_le_right
  le_inf _ _ _ := le_inf
  le_sup_inf
    | lift _, lift _, lift _ => LE.lift le_sup_inf
    | lift a, lift b, comp c => LE.lift <| by simp [sup_comm, sup_assoc]
    | lift a, comp b, lift c => LE.lift <| by simp [sup_left_comm (a := b \ a), sup_comm (a := b \ a)]
    | lift a, comp b, comp c => LE.comp <| by rw [sup_sdiff]
    | comp a, lift b, lift c => LE.comp <| by rw [sdiff_inf]
    | comp a, lift b, comp c => LE.comp <| by rw [sdiff_sdiff_right']
    | comp a, comp b, lift c => LE.comp <| by rw [sdiff_sdiff_right', sup_comm]
    | comp _, comp _, comp _ => LE.comp (inf_sup_left _ _ _).le
Похожие утверждения