Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 11:10 a057441e

View on Github →

feat(order/basic): Notation for order_dual (#13798) Define αᵒᵈ as notation for order_dual α and replace current uses. Zulip poll

Estimated changes

modified theorem pow_le_one'
modified theorem pow_lt_one'
modified def order_iso.inv
modified theorem order_dual.of_dual_smul
modified theorem prime_spectrum.gc
modified theorem prime_spectrum.gc_set
modified theorem convex_Ici
modified theorem convex_Ioi
modified theorem strict_convex_Ici
modified def order_iso.fin_equiv
modified theorem finset.inf'_const
modified theorem finset.inf'_le
modified theorem finset.inf'_le_iff
modified theorem finset.inf'_lt_iff
modified theorem finset.inf_eq_infi
modified theorem finset.inf_id_eq_Inf
modified theorem finset.inf_top
modified theorem finset.le_inf'
modified theorem finset.lt_inf'_iff
modified theorem finset.lt_min'_iff
modified theorem finset.mem_of_min
modified theorem finset.min'_eq_inf'
modified theorem infi_eq_infi_finset
modified theorem fintype.card_order_dual
modified def list.argmin
modified theorem list.le_min_of_le_forall
modified theorem ordnode.bounded.dual_iff
modified theorem ordnode.valid'.dual
modified theorem ordnode.valid'.dual_iff
modified theorem ordnode.valid.dual
modified theorem ordnode.valid.dual_iff
modified def order_iso.inv_ennreal
modified def ereal.neg_order_iso
modified theorem set.Iic_subset_Iic
modified theorem set.Ioi.infinite
modified theorem with_bot.range_coe
modified def linear_map.tunnel
modified theorem exists_glb_Ioi
modified theorem is_glb_Ioi
modified theorem is_least_singleton
modified theorem is_lub_empty
modified theorem le_glb_Ioi
modified theorem lower_bounds_empty
modified theorem not_bdd_below_iff'
modified def Lattice.dual
modified theorem Inf_sup_eq
modified theorem infi_sup_eq
modified theorem sup_Inf_eq
modified theorem sup_infi_eq
modified theorem Inf_eq_bot
modified theorem Inf_eq_infi'
modified theorem Inf_eq_infi
modified theorem Inf_image'
modified theorem Inf_sUnion
modified theorem Sup_eq_bot
modified theorem Sup_image
modified theorem inf_eq_infi
modified theorem infi_bool_eq
modified theorem infi_comm
modified theorem infi_of_empty
modified theorem infi_top
modified theorem le_Inf_inter
modified theorem supr_and
modified theorem supr_bot
modified theorem supr_const
modified def concept.swap_equiv
modified theorem cinfi_const
modified theorem cinfi_set
modified theorem of_dual_covby_of_dual_iff
modified theorem of_dual_wcovby_of_dual_iff
modified theorem filter.at_bot_Iio_eq
modified theorem filter.at_bot_basis'
modified theorem filter.at_bot_basis
modified theorem is_min_on.infi_eq
modified theorem order_hom.gfp_gfp
modified theorem grade_of_dual
modified def order_hom.dual_iso
modified theorem order_hom.symm_dual_comp
modified def order_iso.compl
modified def order_iso.dual_dual
modified theorem bot_hom.symm_dual_comp
modified theorem top_hom.symm_dual_comp
modified theorem Inf_hom.symm_dual_comp
modified theorem Sup_hom.symm_dual_comp
modified theorem inf_hom.symm_dual_comp
modified theorem inf_top_hom.symm_dual_comp
modified theorem lattice_hom.symm_dual_comp
modified def sup_bot_hom.dual
modified theorem sup_bot_hom.symm_dual_comp
modified theorem sup_hom.symm_dual_comp
modified theorem inf_assoc
modified theorem inf_comm
modified theorem inf_idem
modified theorem inf_ind
modified theorem inf_le_iff
modified theorem inf_lt_iff
modified theorem le_inf_iff
modified theorem lt_inf_iff
modified theorem is_bot_of_dual_iff
modified theorem is_bot_or_exists_lt
modified theorem is_max_of_dual_iff
modified theorem is_min_of_dual_iff
modified theorem is_top_of_dual_iff
modified theorem max_cases
modified theorem max_eq_iff
modified theorem max_lt_max_left_iff
modified theorem max_lt_max_right_iff
modified theorem min_lt_min
modified theorem antitone_nat_of_succ_le
modified theorem strict_anti_nat_of_succ_lt
modified theorem strict_mono_nat_of_lt_succ
modified theorem order_dual.le_to_dual
modified theorem order_dual.lt_to_dual
modified def order_dual.of_dual
modified theorem order_dual.of_dual_inj
modified def order_dual.to_dual
modified theorem order_dual.to_dual_inj
modified theorem order_dual.to_dual_le
modified theorem order_dual.to_dual_lt
modified theorem order_dual.to_dual_of_dual
modified theorem order.le_pred_iff_eq_bot
modified theorem order.pred_lt_iff_ne_bot
modified def upper_set.Ici_Sup_hom
modified def upper_set.Ici_sup_hom
modified def add_valuation
modified theorem closure_Iio'
modified theorem disjoint_nhds_at_bot
modified theorem frontier_Ici_subset
modified theorem inf_nhds_at_bot
modified theorem is_compact.Sup_mem
modified theorem Liminf_nhds
modified theorem is_bounded_ge_nhds
modified theorem tendsto_at_bot_csupr
modified theorem tendsto_at_bot_is_lub
modified theorem tendsto_at_top_cinfi
modified theorem tendsto_at_top_is_glb