Commit 2026-08-10 08:17 5ff60493

View on Github →

chore(Order/SymmDiff): use to_dual (#41775) This PR generates bihimp from symmDiff using to_dual.

Estimated changes

deleted theorem Codisjoint.bihimp_eq_inf
deleted theorem IsCompl.bihimp_eq_bot
deleted theorem Pi.bihimp_apply
deleted theorem Pi.bihimp_def
deleted def bihimp
deleted theorem bihimp_bihimp_sup
deleted theorem bihimp_bot
deleted theorem bihimp_comm
deleted theorem bihimp_def
deleted theorem bihimp_eq_sup_himp_inf
deleted theorem bihimp_eq_top
deleted theorem bihimp_fst
deleted theorem bihimp_himp_eq_inf
deleted theorem bihimp_hnot_self
deleted theorem bihimp_inf_sup
deleted theorem bihimp_of_ge
deleted theorem bihimp_of_le
deleted theorem bihimp_self
deleted theorem bihimp_snd
deleted theorem bihimp_top
deleted theorem bihimp_triangle
deleted theorem bot_bihimp
deleted theorem compl_bihimp_self
deleted theorem himp_bihimp
deleted theorem himp_bihimp_eq_inf
deleted theorem inf_le_bihimp
deleted theorem le_bihimp
deleted theorem le_bihimp_iff
deleted theorem ofDual_symmDiff
deleted theorem sup_bihimp_bihimp
deleted theorem sup_himp_bihimp
deleted theorem sup_inf_bihimp
deleted theorem symmDiff_top'
modified theorem symmDiff_top
deleted theorem toDual_bihimp
deleted theorem top_bihimp
deleted theorem top_symmDiff'
modified theorem top_symmDiff