Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-25 08:17 8cd94b84

View on Github →

feat(order/symm_diff): Heyting bi-implication (#16544) Define bihimp, the Heyting bi-implication operator. This is dual to symm_diff and generalizes iff on propositions. Delete order.imp as all the material there is now fully superseded by the Heyting algebra material (himp, defined in order.heyting.basic).

Estimated changes

added theorem compl_himp
added theorem compl_himp_compl
modified theorem compl_sdiff
added theorem compl_sdiff_compl
added theorem is_compl_iff
added theorem himp_idem
deleted def lattice.biimp
deleted theorem lattice.biimp_comm
deleted theorem lattice.biimp_eq_iff
deleted theorem lattice.biimp_eq_top_iff
deleted theorem lattice.biimp_mp
deleted theorem lattice.biimp_mpr
deleted theorem lattice.biimp_self
deleted theorem lattice.biimp_symm
deleted theorem lattice.bot_imp
deleted theorem lattice.compl_biimp
deleted theorem lattice.compl_biimp_compl
deleted theorem lattice.compl_imp
deleted theorem lattice.compl_imp_compl
deleted theorem lattice.compl_sdiff
deleted theorem lattice.compl_symm_diff
deleted def lattice.imp
deleted theorem lattice.imp_bot
deleted theorem lattice.imp_eq_arrow
deleted theorem lattice.imp_eq_bot_iff
deleted theorem lattice.imp_eq_top_iff
deleted theorem lattice.imp_inf_le
deleted theorem lattice.imp_mono
deleted theorem lattice.imp_self
deleted theorem lattice.imp_top
deleted theorem lattice.inf_imp_eq
deleted theorem lattice.le_imp_iff
deleted theorem lattice.top_imp
added def bihimp
added theorem bihimp_assoc
added theorem bihimp_bihimp_self
added theorem bihimp_bihimp_sup
added theorem bihimp_bot
added theorem bihimp_comm
added theorem bihimp_def
added theorem bihimp_eq'
added theorem bihimp_eq
added theorem bihimp_eq_bot
added theorem bihimp_eq_inf
added theorem bihimp_eq_inf_himp_inf
added theorem bihimp_eq_left
added theorem bihimp_eq_right
added theorem bihimp_eq_top
added theorem bihimp_fst
added theorem bihimp_himp_eq_inf
added theorem bihimp_himp_left
added theorem bihimp_himp_right
added theorem bihimp_hnot_self
added theorem bihimp_iff_iff
added theorem bihimp_inf_sup
added theorem bihimp_le_iff_left
added theorem bihimp_le_iff_right
added theorem bihimp_left_comm
added theorem bihimp_left_inj
added theorem bihimp_left_injective
added theorem bihimp_left_involutive
added theorem bihimp_left_surjective
added theorem bihimp_of_ge
added theorem bihimp_of_le
added theorem bihimp_right_comm
added theorem bihimp_right_inj
added theorem bihimp_right_injective
added theorem bihimp_self
added theorem bihimp_snd
added theorem bihimp_top
added theorem bihimp_triangle
added theorem bot_bihimp
added theorem codisjoint_bihimp_sup
added theorem compl_bihimp
added theorem compl_bihimp_compl
added theorem compl_bihimp_self
modified theorem compl_symm_diff
added theorem compl_symm_diff_compl
added theorem himp_bihimp
added theorem himp_bihimp_eq_inf
added theorem himp_bihimp_left
added theorem himp_bihimp_right
added theorem inf_himp_bihimp
added theorem inf_le_bihimp
added theorem is_compl.bihimp_eq_bot
added theorem le_bihimp
added theorem le_bihimp_iff
added theorem of_dual_bihimp
added theorem of_dual_symm_diff
added theorem pi.bihimp_apply
added theorem pi.bihimp_def
added theorem pi.symm_diff_apply
added theorem pi.symm_diff_def
added theorem sdiff_symm_diff_left
added theorem sdiff_symm_diff_right
deleted theorem sdiff_symm_diff_self
added theorem sup_bihimp_bihimp
added theorem sup_himp_bihimp
added theorem sup_inf_bihimp
added theorem symm_diff_eq'
modified theorem symm_diff_eq_bot
added theorem symm_diff_eq_top
deleted theorem symm_diff_eq_top_iff
added theorem symm_diff_fst
added theorem symm_diff_snd
added theorem to_dual_bihimp
added theorem to_dual_symm_diff
added theorem top_bihimp