Commit 2022-12-01 23:11 7ee8c7b0

View on Github →

feat: port Order.Heyting.Basic (#793) mathlib3 sha 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e

Estimated changes

added theorem Disjoint.sdiff_eq_left
added theorem IsCompl.compl_eq
added theorem IsCompl.eq_compl
added theorem IsCompl.eq_hnot
added theorem IsCompl.hnot_eq
added theorem PUnit.bot_eq
added theorem PUnit.compl_eq
added theorem PUnit.himp_eq
added theorem PUnit.hnot_eq
added theorem PUnit.inf_eq
added theorem PUnit.sdiff_eq
added theorem PUnit.sup_eq
added theorem PUnit.top_eq
added theorem Pi.himp_apply
added theorem Pi.himp_def
added theorem Pi.hnot_apply
added theorem Pi.hnot_def
added theorem bot_himp
added theorem bot_sdiff
added theorem codisjoint_hnot_left
added theorem codisjoint_hnot_right
added theorem compl_anti
added theorem compl_bot
added theorem compl_compl_compl
added theorem compl_iff_not
added theorem compl_inf_eq_bot
added theorem compl_inf_self
added theorem compl_le_compl
added theorem compl_le_himp
added theorem compl_le_hnot
added theorem compl_sup
added theorem compl_sup_compl_le
added theorem compl_sup_distrib
added theorem compl_sup_le_himp
added theorem compl_top
added theorem compl_unique
added theorem disjoint_compl_left
added theorem disjoint_compl_right
added theorem fst_compl
added theorem fst_himp
added theorem fst_hnot
added theorem fst_sdiff
added theorem himp_bot
added theorem himp_compl
added theorem himp_compl_comm
added theorem himp_eq_top_iff
added theorem himp_himp
added theorem himp_idem
added theorem himp_iff_imp
added theorem himp_inf_distrib
added theorem himp_inf_himp_cancel
added theorem himp_inf_himp_inf_le
added theorem himp_inf_le
added theorem himp_inf_self
added theorem himp_le_himp
added theorem himp_le_himp_himp_himp
added theorem himp_le_himp_left
added theorem himp_le_himp_right
added theorem himp_left_comm
added theorem himp_self
added theorem himp_top
added theorem himp_triangle
added theorem hnot_anti
added theorem hnot_bot
added theorem hnot_hnot_hnot
added theorem hnot_hnot_le
added theorem hnot_hnot_sup_distrib
added theorem hnot_inf_distrib
added theorem hnot_le_comm
added theorem hnot_le_hnot
added theorem hnot_sdiff
added theorem hnot_sdiff_comm
added theorem hnot_sup_self
added theorem hnot_top
added theorem inf_compl_eq_bot
added theorem inf_compl_self
added theorem inf_himp
added theorem inf_himp_le
added theorem inf_sdiff_left
added theorem inf_sdiff_right
added theorem inf_sdiff_sup_left
added theorem inf_sdiff_sup_right
added theorem le_compl_comm
added theorem le_compl_compl
added theorem le_himp
added theorem le_himp_comm
added theorem le_himp_himp
added theorem le_himp_iff'
added theorem le_himp_iff
added theorem le_himp_iff_left
added theorem le_hnot_inf_hnot
added theorem le_sdiff_sup
added theorem le_sup_sdiff
added theorem le_sup_sdiff_sup_sdiff
added theorem of_dual_compl
added theorem of_dual_himp
added theorem of_dual_hnot
added theorem sdiff_bot
added theorem sdiff_eq_bot_iff
added theorem sdiff_idem
added theorem sdiff_inf
added theorem sdiff_inf_distrib
added theorem sdiff_inf_self_left
added theorem sdiff_inf_self_right
added theorem sdiff_le
added theorem sdiff_le_comm
added theorem sdiff_le_hnot
added theorem sdiff_le_iff'
added theorem sdiff_le_iff
added theorem sdiff_le_iff_left
added theorem sdiff_le_inf_hnot
added theorem sdiff_le_sdiff
added theorem sdiff_le_sdiff_left
added theorem sdiff_le_sdiff_right
added theorem sdiff_right_comm
added theorem sdiff_sdiff
added theorem sdiff_sdiff_comm
added theorem sdiff_sdiff_le
added theorem sdiff_sdiff_left
added theorem sdiff_sdiff_self
added theorem sdiff_self
added theorem sdiff_sup_cancel
added theorem sdiff_sup_sdiff_cancel
added theorem sdiff_sup_self
added theorem sdiff_top
added theorem sdiff_triangle
added theorem snd_compl
added theorem snd_himp
added theorem snd_hnot
added theorem snd_sdiff
added theorem sup_compl_le_himp
added theorem sup_himp_distrib
added theorem sup_himp_self_left
added theorem sup_himp_self_right
added theorem sup_hnot_self
added theorem sup_sdiff
added theorem sup_sdiff_cancel'
added theorem sup_sdiff_cancel_right
added theorem sup_sdiff_distrib
added theorem sup_sdiff_eq_sup
added theorem sup_sdiff_left
added theorem sup_sdiff_left_self
added theorem sup_sdiff_right
added theorem sup_sdiff_right_self
added theorem sup_sdiff_self
added theorem to_dual_compl
added theorem to_dual_hnot
added theorem to_dual_sdiff
added theorem top_himp
added theorem top_sdiff'