instBiheytingAlgebra — Mathlib

Lean4
instance instBiheytingAlgebra : BiheytingAlgebra PUnit.{u + 1} :=
  { PUnit.instLinearOrder.{u} with top := unit, bot := unit, sup := fun _ _ => unit, inf := fun _ _ => unit,
    compl := fun _ => unit, sdiff := fun _ _ => unit, hnot := fun _ => unit, himp := fun _ _ => unit,
    le_top := fun _ => trivial, le_sup_left := fun _ _ => trivial, le_sup_right := fun _ _ => trivial,
    sup_le := fun _ _ _ _ _ => trivial, inf_le_left := fun _ _ => trivial, inf_le_right := fun _ _ => trivial,
    le_inf := fun _ _ _ _ _ => trivial, bot_le := fun _ => trivial, le_himp_iff := fun _ _ _ => Iff.rfl,
    himp_bot := fun _ => rfl, top_sdiff := fun _ => rfl, sdiff_le_iff := fun _ _ _ => Iff.rfl }
Похожие утверждения