Lean4
/-- Turn minimal axioms for `CompletelyDistribLattice` into minimal axioms for
`CompleteDistribLattice`. -/
abbrev toCompleteDistribLattice : CompleteDistribLattice.MinimalAxioms α
where
__ := minAx
inf_sSup_le_iSup_inf a
s := by
let _ := minAx.toCompleteLattice
calc
_ =
⨅ i : ULift.{u} Bool,
⨆ j :
match i with
| .up true => PUnit.{u + 1}
| .up false => s,
match i with
| .up true => a
| .up false => j :=
by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]
_ ≤ _ := by
simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
exact fun x ↦ le_biSup _ (x (.up false)).2
iInf_sup_le_sup_sInf a
s := by
let _ := minAx.toCompleteLattice
calc
_ ≤
⨆ i : ULift.{u} Bool,
⨅ j :
match i with
| .up true => PUnit.{u + 1}
| .up false => s,
match i with
| .up true => a
| .up false => j :=
by
simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
exact fun x ↦ biInf_le _ (x (.up false)).2
_ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]
