Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-19 15:12 9dbc6069

View on Github →

refactor(*): drop lattice namespace (#2166)

  • refactor(*): drop lattice namespace Other changes:
  • rename *neg* to *compl* in boolean_algebra. I didn't touch sub in boolean_algebra; should it become sdiff?
  • Fix some compile failures
  • Fix the rest of compile failures Drop real.Sup and real.Inf, define instances instead.
  • fix build
  • fix build
  • Fix build

Estimated changes

added theorem real.Inf_def
modified theorem real.Inf_empty
modified theorem real.Inf_of_not_bdd_below
added theorem real.Sup_def
modified theorem real.Sup_empty
modified theorem real.Sup_of_not_bdd_above
modified theorem real.Sup_univ
added theorem compl_bot
added theorem compl_compl'
added theorem compl_inf
added theorem compl_inf_eq_bot
added theorem compl_inj
added theorem compl_inj_iff
added theorem compl_le_compl
added theorem compl_le_compl_iff_le
added theorem compl_le_iff_compl_le
added theorem compl_le_of_compl_le
added theorem compl_sup
added theorem compl_sup_eq_top
added theorem compl_top
added theorem compl_unique
added theorem inf_compl_eq_bot
deleted theorem lattice.inf_neg_eq_bot
deleted theorem lattice.le_neg_of_le_neg
deleted theorem lattice.neg_bot
deleted theorem lattice.neg_eq_neg_iff
deleted theorem lattice.neg_eq_neg_of_eq
deleted theorem lattice.neg_inf
deleted theorem lattice.neg_inf_eq_bot
deleted theorem lattice.neg_le_iff_neg_le
deleted theorem lattice.neg_le_neg
deleted theorem lattice.neg_le_neg_iff_le
deleted theorem lattice.neg_le_of_neg_le
deleted theorem lattice.neg_neg
deleted theorem lattice.neg_sup
deleted theorem lattice.neg_sup_eq_top
deleted theorem lattice.neg_top
deleted theorem lattice.neg_unique
deleted theorem lattice.sub_eq
deleted theorem lattice.sub_eq_left
deleted theorem lattice.sub_le_sub
deleted theorem lattice.sup_neg_eq_top
deleted theorem lattice.sup_sub_same
added theorem le_compl_of_le_compl
added theorem sub_eq
added theorem sub_eq_left
added theorem sup_compl_eq_top
added theorem sup_sub_same
added theorem bot_inf_eq
added theorem bot_le
added theorem bot_lt_iff_ne_bot
added theorem bot_sup_eq
added theorem bot_unique
added theorem bounded_lattice.ext
added theorem eq_bot_iff
added theorem eq_bot_mono
added theorem eq_top_iff
added theorem eq_top_mono
added theorem inf_bot_eq
added theorem inf_eq_top_iff
added theorem inf_top_eq
deleted theorem lattice.bot_inf_eq
deleted theorem lattice.bot_le
deleted theorem lattice.bot_lt_iff_ne_bot
deleted theorem lattice.bot_sup_eq
deleted theorem lattice.bot_unique
deleted theorem lattice.eq_bot_iff
deleted theorem lattice.eq_bot_mono
deleted theorem lattice.eq_top_iff
deleted theorem lattice.eq_top_mono
deleted theorem lattice.inf_bot_eq
deleted theorem lattice.inf_eq_top_iff
deleted theorem lattice.inf_top_eq
deleted theorem lattice.le_bot_iff
deleted theorem lattice.le_top
deleted theorem lattice.lt_top_iff_ne_top
deleted theorem lattice.monotone_and
deleted theorem lattice.monotone_or
deleted theorem lattice.ne_bot_of_gt
deleted theorem lattice.ne_top_of_lt
deleted theorem lattice.not_lt_bot
deleted theorem lattice.not_top_lt
deleted theorem lattice.order_bot.ext
deleted theorem lattice.order_bot.ext_bot
deleted theorem lattice.order_top.ext
deleted theorem lattice.order_top.ext_top
deleted theorem lattice.sup_bot_eq
deleted theorem lattice.sup_eq_bot_iff
deleted theorem lattice.sup_top_eq
deleted theorem lattice.top_inf_eq
deleted theorem lattice.top_le_iff
deleted theorem lattice.top_sup_eq
deleted theorem lattice.top_unique
added theorem le_bot_iff
added theorem le_top
added theorem lt_top_iff_ne_top
added theorem monotone_and
added theorem monotone_or
added theorem ne_bot_of_gt
added theorem ne_bot_of_le_ne_bot
added theorem ne_top_of_le_ne_top
added theorem ne_top_of_lt
added theorem not_lt_bot
added theorem not_top_lt
added theorem order_bot.ext
added theorem order_bot.ext_bot
added theorem order_top.ext
added theorem order_top.ext_top
added theorem sup_bot_eq
added theorem sup_eq_bot_iff
added theorem sup_top_eq
added theorem top_inf_eq
added theorem top_le_iff
added theorem top_sup_eq
added theorem top_unique
added theorem Inf_sup_Inf
added theorem Inf_sup_eq
added theorem Sup_inf_Sup
added theorem Sup_inf_eq
added theorem compl_Inf
added theorem compl_Sup
added theorem compl_infi
added theorem compl_supr
added theorem inf_Sup_eq
deleted theorem lattice.Inf_sup_Inf
deleted theorem lattice.Inf_sup_eq
deleted theorem lattice.Sup_inf_Sup
deleted theorem lattice.Sup_inf_eq
deleted theorem lattice.inf_Sup_eq
deleted theorem lattice.neg_Inf
deleted theorem lattice.neg_Sup
deleted theorem lattice.neg_infi
deleted theorem lattice.neg_supr
deleted theorem lattice.sup_Inf_eq
added theorem sup_Inf_eq
added def Inf
added theorem Inf_Prop_eq
added theorem Inf_apply
added theorem Inf_empty
added theorem Inf_eq_bot
added theorem Inf_eq_infi
added theorem Inf_eq_top
added theorem Inf_image
added theorem Inf_insert
added theorem Inf_le
added theorem Inf_le_Inf
added theorem Inf_le_Sup
added theorem Inf_le_of_le
added theorem Inf_lt_iff
added theorem Inf_pair
added theorem Inf_range
added theorem Inf_singleton
added theorem Inf_union
added theorem Inf_univ
added def Sup
added theorem Sup_Prop_eq
added theorem Sup_apply
added theorem Sup_empty
added theorem Sup_eq_bot
added theorem Sup_eq_supr
added theorem Sup_eq_top
added theorem Sup_image
added theorem Sup_insert
added theorem Sup_inter_le
added theorem Sup_le
added theorem Sup_le_Sup
added theorem Sup_le_iff
added theorem Sup_pair
added theorem Sup_range
added theorem Sup_singleton
added theorem Sup_union
added theorem Sup_univ
added theorem binfi_inf
added theorem has_Inf_to_nonempty
added theorem has_Sup_to_nonempty
added theorem inf_infi
added def infi
added theorem infi_Prop_eq
added theorem infi_and
added theorem infi_apply
added theorem infi_bool_eq
added theorem infi_comm
added theorem infi_congr_Prop
added theorem infi_const
added theorem infi_empty
added theorem infi_emptyset
added theorem infi_eq_bot
added theorem infi_eq_dif
added theorem infi_eq_if
added theorem infi_eq_top
added theorem infi_exists
added theorem infi_false
added theorem infi_image
added theorem infi_inf
added theorem infi_inf_eq
added theorem infi_infi_eq_left
added theorem infi_infi_eq_right
added theorem infi_insert
added theorem infi_le'
added theorem infi_le
added theorem infi_le_infi2
added theorem infi_le_infi
added theorem infi_le_infi_const
added theorem infi_le_infi_of_subset
added theorem infi_le_of_le
added theorem infi_lt_iff
added theorem infi_neg
added theorem infi_or
added theorem infi_pair
added theorem infi_pos
added theorem infi_prod
added theorem infi_range
added theorem infi_sigma
added theorem infi_singleton
added theorem infi_subtype'
added theorem infi_subtype
added theorem infi_sum
added theorem infi_top
added theorem infi_true
added theorem infi_union
added theorem infi_unit
added theorem infi_univ
added theorem is_glb.Inf_eq
added theorem is_glb.infi_eq
added theorem is_glb_Inf
added theorem is_glb_infi
added theorem is_lub.Sup_eq
added theorem is_lub.supr_eq
added theorem is_lub_Sup
added theorem is_lub_supr
deleted def lattice.Inf
deleted theorem lattice.Inf_Prop_eq
deleted theorem lattice.Inf_apply
deleted theorem lattice.Inf_empty
deleted theorem lattice.Inf_eq_bot
deleted theorem lattice.Inf_eq_infi
deleted theorem lattice.Inf_eq_top
deleted theorem lattice.Inf_image
deleted theorem lattice.Inf_insert
deleted theorem lattice.Inf_le
deleted theorem lattice.Inf_le_Inf
deleted theorem lattice.Inf_le_Sup
deleted theorem lattice.Inf_le_of_le
deleted theorem lattice.Inf_lt_iff
deleted theorem lattice.Inf_pair
deleted theorem lattice.Inf_range
deleted theorem lattice.Inf_singleton
deleted theorem lattice.Inf_union
deleted theorem lattice.Inf_univ
deleted def lattice.Sup
deleted theorem lattice.Sup_Prop_eq
deleted theorem lattice.Sup_apply
deleted theorem lattice.Sup_empty
deleted theorem lattice.Sup_eq_bot
deleted theorem lattice.Sup_eq_supr
deleted theorem lattice.Sup_eq_top
deleted theorem lattice.Sup_image
deleted theorem lattice.Sup_insert
deleted theorem lattice.Sup_inter_le
deleted theorem lattice.Sup_le
deleted theorem lattice.Sup_le_Sup
deleted theorem lattice.Sup_le_iff
deleted theorem lattice.Sup_pair
deleted theorem lattice.Sup_range
deleted theorem lattice.Sup_singleton
deleted theorem lattice.Sup_union
deleted theorem lattice.Sup_univ
deleted theorem lattice.binfi_inf
deleted theorem lattice.inf_infi
deleted def lattice.infi
deleted theorem lattice.infi_Prop_eq
deleted theorem lattice.infi_and
deleted theorem lattice.infi_apply
deleted theorem lattice.infi_bool_eq
deleted theorem lattice.infi_comm
deleted theorem lattice.infi_congr_Prop
deleted theorem lattice.infi_const
deleted theorem lattice.infi_empty
deleted theorem lattice.infi_emptyset
deleted theorem lattice.infi_eq_bot
deleted theorem lattice.infi_eq_dif
deleted theorem lattice.infi_eq_if
deleted theorem lattice.infi_eq_top
deleted theorem lattice.infi_exists
deleted theorem lattice.infi_false
deleted theorem lattice.infi_image
deleted theorem lattice.infi_inf
deleted theorem lattice.infi_inf_eq
deleted theorem lattice.infi_infi_eq_left
deleted theorem lattice.infi_insert
deleted theorem lattice.infi_le'
deleted theorem lattice.infi_le
deleted theorem lattice.infi_le_infi2
deleted theorem lattice.infi_le_infi
deleted theorem lattice.infi_le_of_le
deleted theorem lattice.infi_lt_iff
deleted theorem lattice.infi_neg
deleted theorem lattice.infi_or
deleted theorem lattice.infi_pair
deleted theorem lattice.infi_pos
deleted theorem lattice.infi_prod
deleted theorem lattice.infi_range
deleted theorem lattice.infi_sigma
deleted theorem lattice.infi_singleton
deleted theorem lattice.infi_subtype'
deleted theorem lattice.infi_subtype
deleted theorem lattice.infi_sum
deleted theorem lattice.infi_top
deleted theorem lattice.infi_true
deleted theorem lattice.infi_union
deleted theorem lattice.infi_unit
deleted theorem lattice.infi_univ
deleted theorem lattice.is_glb_Inf
deleted theorem lattice.is_glb_infi
deleted theorem lattice.is_lub_Sup
deleted theorem lattice.is_lub_supr
deleted theorem lattice.le_Inf
deleted theorem lattice.le_Inf_iff
deleted theorem lattice.le_Inf_inter
deleted theorem lattice.le_Sup
deleted theorem lattice.le_Sup_of_le
deleted theorem lattice.le_infi
deleted theorem lattice.le_infi_iff
deleted theorem lattice.le_supr'
deleted theorem lattice.le_supr
deleted theorem lattice.le_supr_iff
deleted theorem lattice.le_supr_of_le
deleted theorem lattice.lt_Sup_iff
deleted theorem lattice.lt_supr_iff
deleted def lattice.supr
deleted theorem lattice.supr_Prop_eq
deleted theorem lattice.supr_and
deleted theorem lattice.supr_apply
deleted theorem lattice.supr_bool_eq
deleted theorem lattice.supr_bot
deleted theorem lattice.supr_comm
deleted theorem lattice.supr_congr_Prop
deleted theorem lattice.supr_const
deleted theorem lattice.supr_empty
deleted theorem lattice.supr_emptyset
deleted theorem lattice.supr_eq_bot
deleted theorem lattice.supr_eq_dif
deleted theorem lattice.supr_eq_if
deleted theorem lattice.supr_eq_top
deleted theorem lattice.supr_exists
deleted theorem lattice.supr_false
deleted theorem lattice.supr_image
deleted theorem lattice.supr_insert
deleted theorem lattice.supr_le
deleted theorem lattice.supr_le_iff
deleted theorem lattice.supr_le_supr2
deleted theorem lattice.supr_le_supr
deleted theorem lattice.supr_neg
deleted theorem lattice.supr_or
deleted theorem lattice.supr_pair
deleted theorem lattice.supr_pos
deleted theorem lattice.supr_prod
deleted theorem lattice.supr_range
deleted theorem lattice.supr_sigma
deleted theorem lattice.supr_singleton
deleted theorem lattice.supr_subtype'
deleted theorem lattice.supr_subtype
deleted theorem lattice.supr_sum
deleted theorem lattice.supr_sup_eq
deleted theorem lattice.supr_supr_eq_left
deleted theorem lattice.supr_true
deleted theorem lattice.supr_union
deleted theorem lattice.supr_unit
deleted theorem lattice.supr_univ
added theorem le_Inf
added theorem le_Inf_iff
added theorem le_Inf_inter
added theorem le_Sup
added theorem le_Sup_of_le
added theorem le_infi
added theorem le_infi_iff
added theorem le_supr'
added theorem le_supr
added theorem le_supr_iff
added theorem le_supr_of_le
added theorem lt_Sup_iff
added theorem lt_supr_iff
added def ord_continuous
added theorem ord_continuous_mono
added theorem ord_continuous_sup
added def supr
added theorem supr_Prop_eq
added theorem supr_and
added theorem supr_apply
added theorem supr_bool_eq
added theorem supr_bot
added theorem supr_comm
added theorem supr_congr_Prop
added theorem supr_const
added theorem supr_empty
added theorem supr_emptyset
added theorem supr_eq_bot
added theorem supr_eq_dif
added theorem supr_eq_if
added theorem supr_eq_top
added theorem supr_exists
added theorem supr_false
added theorem supr_image
added theorem supr_insert
added theorem supr_le
added theorem supr_le_iff
added theorem supr_le_supr2
added theorem supr_le_supr
added theorem supr_le_supr_const
added theorem supr_le_supr_of_subset
added theorem supr_neg
added theorem supr_or
added theorem supr_pair
added theorem supr_pos
added theorem supr_prod
added theorem supr_range
added theorem supr_sigma
added theorem supr_singleton
added theorem supr_subtype'
added theorem supr_subtype
added theorem supr_sum
added theorem supr_sup_eq
added theorem supr_supr_eq_left
added theorem supr_supr_eq_right
added theorem supr_true
added theorem supr_union
added theorem supr_unit
added theorem supr_univ
added theorem Inf_nat_def
added theorem Sup_nat_def
added theorem cInf_Ici
added theorem cInf_insert
added theorem cInf_intro
added theorem cInf_le
added theorem cInf_le_cInf
added theorem cInf_le_cSup
added theorem cInf_le_of_le
added theorem cInf_lt_of_lt
added theorem cInf_singleton
added theorem cInf_union
added theorem cSup_Iic
added theorem cSup_empty
added theorem cSup_insert
added theorem cSup_inter_le
added theorem cSup_intro'
added theorem cSup_intro
added theorem cSup_le
added theorem cSup_le_cSup
added theorem cSup_le_iff
added theorem cSup_singleton
added theorem cSup_union
added theorem cinfi_const
added theorem cinfi_le
added theorem cinfi_le_cinfi
added theorem csupr_const
added theorem csupr_le
added theorem csupr_le_csupr
added theorem exists_lt_of_cInf_lt
added theorem exists_lt_of_cinfi_lt
added theorem exists_lt_of_lt_cSup
added theorem exists_lt_of_lt_csupr
added theorem is_glb.cInf_eq
added theorem is_glb_cInf
added theorem is_greatest.cSup_eq
added theorem is_least.cInf_eq
added theorem is_lub.cSup_eq
added theorem is_lub_cSup
deleted theorem lattice.Inf_nat_def
deleted theorem lattice.Sup_nat_def
deleted theorem lattice.cInf_Ici
deleted theorem lattice.cInf_insert
deleted theorem lattice.cInf_intro
deleted theorem lattice.cInf_le
deleted theorem lattice.cInf_le_cInf
deleted theorem lattice.cInf_le_cSup
deleted theorem lattice.cInf_le_of_le
deleted theorem lattice.cInf_lt_of_lt
deleted theorem lattice.cInf_singleton
deleted theorem lattice.cInf_union
deleted theorem lattice.cSup_Iic
deleted theorem lattice.cSup_empty
deleted theorem lattice.cSup_insert
deleted theorem lattice.cSup_inter_le
deleted theorem lattice.cSup_intro'
deleted theorem lattice.cSup_intro
deleted theorem lattice.cSup_le
deleted theorem lattice.cSup_le_cSup
deleted theorem lattice.cSup_le_iff
deleted theorem lattice.cSup_singleton
deleted theorem lattice.cSup_union
deleted theorem lattice.cinfi_const
deleted theorem lattice.cinfi_le
deleted theorem lattice.cinfi_le_cinfi
deleted theorem lattice.csupr_const
deleted theorem lattice.csupr_le
deleted theorem lattice.csupr_le_csupr
deleted theorem lattice.is_glb_cInf
deleted theorem lattice.is_lub_cSup
deleted theorem lattice.le_cInf
deleted theorem lattice.le_cInf_iff
deleted theorem lattice.le_cInf_inter
deleted theorem lattice.le_cSup
deleted theorem lattice.le_cSup_of_le
deleted theorem lattice.le_cinfi
deleted theorem lattice.le_csupr
deleted theorem lattice.lt_cSup_of_lt
added theorem le_cInf
added theorem le_cInf_iff
added theorem le_cInf_inter
added theorem le_cSup
added theorem le_cSup_of_le
added theorem le_cinfi
added theorem le_csupr
added theorem lt_cSup_of_lt
added theorem fixed_points.next_eq
added theorem fixed_points.next_le
added theorem fixed_points.prev_eq
added theorem fixed_points.prev_le
added def fixed_points
added def gfp
added theorem gfp_comp
added theorem gfp_eq
added theorem gfp_gfp
added theorem gfp_induct
added theorem gfp_le
deleted def lattice.gfp
deleted theorem lattice.gfp_comp
deleted theorem lattice.gfp_eq
deleted theorem lattice.gfp_gfp
deleted theorem lattice.gfp_induct
deleted theorem lattice.gfp_le
deleted theorem lattice.le_gfp
deleted theorem lattice.le_lfp
deleted def lattice.lfp
deleted theorem lattice.lfp_comp
deleted theorem lattice.lfp_eq
deleted theorem lattice.lfp_induct
deleted theorem lattice.lfp_le
deleted theorem lattice.lfp_lfp
deleted theorem lattice.monotone_gfp
deleted theorem lattice.monotone_lfp
added theorem le_gfp
added theorem le_lfp
added def lfp
added theorem lfp_comp
added theorem lfp_eq
added theorem lfp_induct
added theorem lfp_le
added theorem lfp_lfp
added theorem monotone_gfp
added theorem monotone_lfp
added theorem directed_of_inf
added theorem directed_of_mono
added theorem directed_of_sup
added theorem eq_of_sup_eq_inf_eq
added theorem inf_assoc
added theorem inf_comm
added theorem inf_eq_min
added theorem inf_idem
added theorem inf_le_inf
added theorem inf_le_inf_left
added theorem inf_le_inf_right
added theorem inf_le_left'
added theorem inf_le_left
added theorem inf_le_left_of_le
added theorem inf_le_right'
added theorem inf_le_right
added theorem inf_le_right_of_le
added theorem inf_left_comm
added theorem inf_of_le_left
added theorem inf_of_le_right
added theorem inf_sup_left
added theorem inf_sup_right
added theorem inf_sup_self
deleted theorem lattice.directed_of_inf
deleted theorem lattice.directed_of_mono
deleted theorem lattice.directed_of_sup
modified theorem lattice.ext
deleted theorem lattice.inf_assoc
deleted theorem lattice.inf_comm
deleted theorem lattice.inf_eq_min
deleted theorem lattice.inf_idem
deleted theorem lattice.inf_le_inf
deleted theorem lattice.inf_le_inf_left
deleted theorem lattice.inf_le_inf_right
deleted theorem lattice.inf_le_left'
deleted theorem lattice.inf_le_left
deleted theorem lattice.inf_le_left_of_le
deleted theorem lattice.inf_le_right'
deleted theorem lattice.inf_le_right
deleted theorem lattice.inf_left_comm
deleted theorem lattice.inf_of_le_left
deleted theorem lattice.inf_of_le_right
deleted theorem lattice.inf_sup_left
deleted theorem lattice.inf_sup_right
deleted theorem lattice.inf_sup_self
deleted theorem lattice.le_inf
deleted theorem lattice.le_inf_iff
deleted theorem lattice.le_inf_sup
deleted theorem lattice.le_of_inf_eq
deleted theorem lattice.le_of_sup_eq
deleted theorem lattice.le_sup_inf
deleted theorem lattice.le_sup_left'
deleted theorem lattice.le_sup_left
deleted theorem lattice.le_sup_left_of_le
deleted theorem lattice.le_sup_right'
deleted theorem lattice.le_sup_right
deleted theorem lattice.lt_inf_iff
deleted theorem lattice.sup_assoc
deleted theorem lattice.sup_comm
deleted theorem lattice.sup_eq_max
deleted theorem lattice.sup_idem
deleted theorem lattice.sup_inf_le
deleted theorem lattice.sup_inf_left
deleted theorem lattice.sup_inf_right
deleted theorem lattice.sup_inf_self
deleted theorem lattice.sup_le
deleted theorem lattice.sup_le_iff
deleted theorem lattice.sup_le_sup
deleted theorem lattice.sup_le_sup_left
deleted theorem lattice.sup_le_sup_right
deleted theorem lattice.sup_left_comm
deleted theorem lattice.sup_lt_iff
deleted theorem lattice.sup_of_le_left
deleted theorem lattice.sup_of_le_right
modified theorem le_antisymm'
added theorem le_inf
added theorem le_inf_iff
added theorem le_inf_sup
added theorem le_of_inf_eq
added theorem le_of_sup_eq
added theorem le_sup_inf
added theorem le_sup_left'
added theorem le_sup_left
added theorem le_sup_left_of_le
added theorem le_sup_right'
added theorem le_sup_right
added theorem le_sup_right_of_le
added theorem lt_inf_iff
added theorem semilattice_inf.ext
added theorem semilattice_sup.ext
added theorem sup_assoc
added theorem sup_comm
added theorem sup_eq_max
added theorem sup_idem
added theorem sup_inf_le
added theorem sup_inf_left
added theorem sup_inf_right
added theorem sup_inf_self
added theorem sup_le
added theorem sup_le_iff
added theorem sup_le_sup
added theorem sup_le_sup_left
added theorem sup_le_sup_right
added theorem sup_left_comm
added theorem sup_lt_iff
added theorem sup_of_le_left
added theorem sup_of_le_right