Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-04 23:36 4eee8bc3

View on Github →

chore(order/complete_lattice): Generalize ⨆/⨅ lemmas to dependent families (#13154) The "bounded supremum" and "bounded infimum" are both instances of nested ⨆/⨅. But they only apply when the inner one runs over a predicate p : ι → Prop, and the function couldn't depend on p. This generalizes to κ : ι → Sort* and allows dependence on κ i. The lemmas are renamed from bsupr/binfi to supr₂/infi₂ to show that they are more general. Some lemmas were missing between ⨆ and ⨅ or between ⨆/⨅ and nested ⨆/⨅, so I'm adding them as well. Renames

Estimated changes

modified theorem set.Inter_congr
modified theorem set.Inter_subset
modified theorem set.Union_congr
modified theorem set.subset_Union
modified theorem Inf_Prop_eq
modified theorem Inf_eq_infi'
modified theorem Inf_eq_infi
modified theorem Inf_image'
modified theorem Inf_image
modified theorem Inf_lt_iff
modified theorem Inf_range
added theorem Inf_sUnion
modified theorem Inf_sup_le_infi_sup
modified theorem Sup_Prop_eq
modified theorem Sup_eq_supr'
modified theorem Sup_eq_supr
modified theorem Sup_image'
modified theorem Sup_image
modified theorem Sup_range
modified theorem Sup_sUnion
added theorem antitone.le_map_Inf
added theorem antitone.le_map_infi
added theorem antitone.map_Sup_le
added theorem antitone.map_supr_le
deleted theorem binfi_le
deleted theorem binfi_le_binfi
deleted theorem binfi_le_of_le
added theorem binfi_mono
deleted theorem bsupr_le
deleted theorem bsupr_le_bsupr'
deleted theorem bsupr_le_bsupr
deleted theorem bsupr_le_supr
added theorem bsupr_mono
modified theorem infi_Prop_eq
modified theorem infi_and
modified theorem infi_comm
modified theorem infi_congr
modified theorem infi_congr_Prop
added theorem infi_const_mono
modified theorem infi_eq_top
modified theorem infi_exists
modified theorem infi_le'
modified theorem infi_le
deleted theorem infi_le_binfi
deleted theorem infi_le_infi2
deleted theorem infi_le_infi
deleted theorem infi_le_infi_const
added theorem infi_le_infi₂
modified theorem infi_le_of_le
modified theorem infi_lt_iff
added theorem infi_mono'
added theorem infi_mono
modified theorem infi_range'
modified theorem infi_range
modified theorem infi_top
modified theorem infi_true
added theorem infi₂_eq_top
added theorem infi₂_le
added theorem infi₂_le_of_le
added theorem infi₂_mono'
added theorem infi₂_mono
modified theorem is_glb.infi_eq
modified theorem is_glb_Inf
modified theorem is_glb_infi
modified theorem is_lub.supr_eq
modified theorem is_lub_Sup
modified theorem is_lub_supr
deleted theorem le_binfi
deleted theorem le_bsupr
deleted theorem le_bsupr_of_le
modified theorem le_infi
modified theorem le_infi_iff
added theorem le_infi₂
added theorem le_infi₂_iff
modified theorem le_supr'
modified theorem le_supr
modified theorem le_supr_of_le
added theorem le_supr₂
added theorem le_supr₂_of_le
modified theorem lt_Sup_iff
added theorem lt_infi_iff
modified theorem lt_supr_iff
deleted theorem monotone.le_map_supr2
deleted theorem monotone.map_infi2_le
modified theorem sup_Inf_le_infi_sup
modified theorem supr_Prop_eq
modified theorem supr_and
modified theorem supr_bot
modified theorem supr_comm
modified theorem supr_congr
modified theorem supr_congr_Prop
added theorem supr_const_mono
modified theorem supr_eq_bot
modified theorem supr_exists
modified theorem supr_inf_le_Sup_inf
modified theorem supr_inf_le_inf_Sup
modified theorem supr_le
modified theorem supr_le_iff
deleted theorem supr_le_supr2
deleted theorem supr_le_supr
deleted theorem supr_le_supr_const
modified theorem supr_lt_iff
added theorem supr_mono'
added theorem supr_mono
modified theorem supr_range'
modified theorem supr_range
modified theorem supr_true
added theorem supr₂_eq_bot
added theorem supr₂_le
added theorem supr₂_le_iff
added theorem supr₂_le_supr
added theorem supr₂_mono'
added theorem supr₂_mono
modified theorem filter.lift_mono'
modified theorem filter.pi_mono