Commit 2023-06-30 23:14 e3c8f983

View on Github →

fix: precedences of ⨆⋃⋂⨅ (#5614)

Estimated changes

modified theorem iUnion_Icc_add_int_cast
modified theorem iUnion_Icc_add_zsmul
modified theorem iUnion_Icc_int_cast
modified theorem iUnion_Icc_zsmul
modified theorem iUnion_Ico_add_int_cast
modified theorem iUnion_Ico_add_zsmul
modified theorem iUnion_Ico_int_cast
modified theorem iUnion_Ico_zsmul
modified theorem iUnion_Ioc_add_int_cast
modified theorem iUnion_Ioc_add_zsmul
modified theorem iUnion_Ioc_int_cast
modified theorem iUnion_Ioc_zsmul
modified theorem Submodule.iInf_orthogonal
modified theorem Submodule.sInf_orthogonal
modified theorem Finset.iInf_coe
modified theorem Finset.iInf_option_toFinset
modified theorem Finset.iInf_singleton
modified theorem Finset.iSup_coe
modified theorem Finset.iSup_option_toFinset
modified theorem Finset.iSup_singleton
modified theorem Finset.set_biInter_coe
modified theorem Finset.set_biUnion_coe
modified theorem Set.iInter_eq_iInter_finset
modified theorem Set.iUnion_eq_iUnion_finset
modified theorem iInf_eq_iInf_finset
modified theorem iSup_eq_iSup_finset
modified theorem Nat.iInf_lt_succ'
modified theorem Nat.iInf_lt_succ
modified theorem Nat.iSup_lt_succ'
modified theorem Nat.iSup_lt_succ
modified theorem Set.biInter_lt_succ'
modified theorem Set.biInter_lt_succ
modified theorem Set.biUnion_lt_succ'
modified theorem Set.biUnion_lt_succ
modified theorem Real.ciInf_const_zero
modified theorem Real.ciInf_empty
modified theorem Real.ciSup_const_zero
modified theorem Real.ciSup_empty
modified theorem ENNReal.cinfi_ne_top
modified theorem ENNReal.csupr_ne_top
modified theorem ENNReal.iInter_Ici_coe_nat
modified theorem ENNReal.iInter_Ioi_coe_nat
modified theorem ENNReal.iSup_coe_nat
modified theorem ENNReal.iSup_eq_zero
modified theorem ENNReal.iSup_zero_eq_zero
modified theorem ENNReal.iUnion_Icc_coe_nat
modified theorem ENNReal.iUnion_Ico_coe_nat
modified theorem ENNReal.iUnion_Iic_coe_nat
modified theorem ENNReal.iUnion_Iio_coe_nat
modified theorem ENNReal.iUnion_Ioc_coe_nat
modified theorem ENNReal.iUnion_Ioo_coe_nat
modified theorem NNReal.iInf_const_zero
modified theorem NNReal.iInf_empty
modified theorem NNReal.iSup_empty
modified theorem NNReal.iSup_of_not_bddAbove
modified theorem Set.biUnion_accumulate
modified theorem Set.iUnion_accumulate
modified theorem IsGLB.biUnion_Ioi_eq
modified theorem IsGLB.iUnion_Ioi_eq
modified theorem IsLUB.biUnion_Iic_eq_Iic
modified theorem IsLUB.biUnion_Iio_eq
modified theorem IsLUB.iUnion_Iio_eq
modified theorem Set.iUnion_Icc_left
modified theorem Set.iUnion_Icc_right
modified theorem Set.iUnion_Ici
modified theorem Set.iUnion_Ico_left
modified theorem Set.iUnion_Ico_right
modified theorem Set.iUnion_Iic
modified theorem Set.iUnion_Iio
modified theorem Set.iUnion_Ioc_left
modified theorem Set.iUnion_Ioc_right
modified theorem Set.iUnion_Ioi
modified theorem Set.iUnion_Ioo_left
modified theorem Set.iUnion_Ioo_right
modified theorem Set.biInter_empty
modified theorem Set.biInter_image
modified theorem Set.biInter_pair
modified theorem Set.biInter_range
modified theorem Set.biInter_singleton
modified theorem Set.biInter_univ
modified theorem Set.biUnion_empty
modified theorem Set.biUnion_image
modified theorem Set.biUnion_of_singleton
modified theorem Set.biUnion_pair
modified theorem Set.biUnion_range
modified theorem Set.biUnion_self
modified theorem Set.biUnion_singleton
modified theorem Set.biUnion_univ
modified theorem Set.iInter_and
modified theorem Set.iInter_comm
modified theorem Set.iInter_congr
modified theorem Set.iInter_const
modified theorem Set.iInter_eq_const
modified theorem Set.iInter_eq_empty_iff
modified theorem Set.iInter_eq_if
modified theorem Set.iInter_eq_univ
modified theorem Set.iInter_mono
modified theorem Set.iInter_of_empty
modified theorem Set.iInter_option
modified theorem Set.iInter_plift_down
modified theorem Set.iInter_plift_up
modified theorem Set.iInter_setOf
modified theorem Set.iInter_subset
modified theorem Set.iInter₂_subset
modified theorem Set.iUnion_and
modified theorem Set.iUnion_comm
modified theorem Set.iUnion_congr
modified theorem Set.iUnion_const
modified theorem Set.iUnion_eq_const
modified theorem Set.iUnion_eq_empty
modified theorem Set.iUnion_eq_if
modified theorem Set.iUnion_eq_range_psigma
modified theorem Set.iUnion_eq_range_sigma
modified theorem Set.iUnion_eq_univ_iff
modified theorem Set.iUnion_image_left
modified theorem Set.iUnion_image_right
modified theorem Set.iUnion_inter_subset
modified theorem Set.iUnion_mono
modified theorem Set.iUnion_nonempty_self
modified theorem Set.iUnion_of_empty
modified theorem Set.iUnion_of_singleton_coe
modified theorem Set.iUnion_option
modified theorem Set.iUnion_plift_down
modified theorem Set.iUnion_plift_up
modified theorem Set.iUnion_setOf
modified theorem Set.iUnion_subset
modified theorem Set.iUnion_subset_iff
modified theorem Set.mem_sUnion
modified theorem Set.sInter_iUnion
modified theorem Set.sUnion_iUnion
modified theorem iInf_iUnion
modified theorem iSup_iUnion
modified theorem sInf_sUnion
modified theorem sSup_sUnion
modified theorem Set.iUnion_div_left_image
modified theorem Set.iUnion_div_right_image
modified theorem Set.iUnion_mul_left_image
modified theorem Set.iUnion_mul_right_image
modified theorem Set.iUnion_inv_smul
modified theorem Set.iUnion_op_smul_set
modified theorem Set.iUnion_smul_left_image
modified theorem Set.iUnion_smul_right_image
modified theorem Set.iUnion_smul_set
modified theorem Set.iUnion_vsub_left_image
modified theorem Set.iUnion_vsub_right_image
modified theorem Set.iUnion_image_inf_left
modified theorem Set.iUnion_image_inf_right
modified theorem Set.iUnion_image_sup_left
modified theorem Set.iUnion_image_sup_right
modified theorem IndexedPartition.iUnion
modified theorem omegaLimit_iUnion
modified theorem Function.bUnion_ptsOfPeriod
modified theorem Doset.union_quotToDoset
modified theorem Finsupp.iSup_lsingle_range
modified theorem Submodule.iSup_eq_span
modified theorem Submodule.iSup_span
modified theorem Encodable.iUnion_decode₂
modified theorem Antitone.iInf_nat_add
modified theorem Equiv.iInf_comp
modified theorem Equiv.iSup_comp
modified theorem IsGLB.iInf_eq
modified theorem IsLUB.iSup_eq
modified theorem Monotone.iSup_nat_add
modified theorem biInf_const
modified theorem biSup_const
modified theorem iInf_Prop_eq
modified theorem iInf_bool_eq
modified theorem iInf_comm
modified theorem iInf_congr
modified theorem iInf_const
modified theorem iInf_const_mono
modified theorem iInf_emptyset
modified theorem iInf_eq_if
modified theorem iInf_exists
modified theorem iInf_ge_eq_iInf_nat_add
modified theorem iInf_iInf_eq_left
modified theorem iInf_iInf_eq_right
modified theorem iInf_inf_eq
modified theorem iInf_le_iInf_of_subset
modified theorem iInf_le_iInf₂
modified theorem iInf_nat_gt_zero_eq
modified theorem iInf_ne_top_subtype
modified theorem iInf_neg
modified theorem iInf_option
modified theorem iInf_option_elim
modified theorem iInf_pair
modified theorem iInf_plift_down
modified theorem iInf_plift_up
modified theorem iInf_pos
modified theorem iInf_prod
modified theorem iInf_range'
modified theorem iInf_range
modified theorem iInf_sigma
modified theorem iInf_singleton
modified theorem iInf_split_single
modified theorem iInf_subtype''
modified theorem iInf_sum
modified theorem iInf_sup_iInf_le
modified theorem iInf_union
modified theorem iInf_univ
modified theorem iInf₂_eq_top
modified theorem iInf₂_le
modified theorem iSup_Prop_eq
modified theorem iSup_bool_eq
modified theorem iSup_comm
modified theorem iSup_comp_le
modified theorem iSup_congr
modified theorem iSup_const
modified theorem iSup_const_le
modified theorem iSup_const_mono
modified theorem iSup_emptyset
modified theorem iSup_eq_if
modified theorem iSup_exists
modified theorem iSup_ge_eq_iSup_nat_add
modified theorem iSup_iInf_le_iInf_iSup
modified theorem iSup_iSup_eq_left
modified theorem iSup_iSup_eq_right
modified theorem iSup_inf_le_inf_sSup
modified theorem iSup_inf_le_sSup_inf
modified theorem iSup_le_iSup_of_subset
modified theorem iSup_nat_gt_zero_eq
modified theorem iSup_ne_bot_subtype
modified theorem iSup_neg
modified theorem iSup_option
modified theorem iSup_option_elim
modified theorem iSup_pair
modified theorem iSup_plift_down
modified theorem iSup_plift_up
modified theorem iSup_pos
modified theorem iSup_prod
modified theorem iSup_range'
modified theorem iSup_range
modified theorem iSup_sigma
modified theorem iSup_singleton
modified theorem iSup_split_single
modified theorem iSup_subtype''
modified theorem iSup_sum
modified theorem iSup_sup_eq
modified theorem iSup_union
modified theorem iSup_univ
modified theorem iSup₂_eq_bot
modified theorem iSup₂_le
modified theorem iSup₂_le_iSup
modified theorem iSup₂_le_iff
modified theorem le_iInf_comp
modified theorem le_iSup_inf_iSup
modified theorem IsGLB.ciInf_eq
modified theorem IsLUB.ciSup_eq
modified theorem ciInf_const
modified theorem ciInf_pos
modified theorem ciInf_subsingleton
modified theorem ciInf_unique
modified theorem ciSup_const
modified theorem ciSup_false
modified theorem ciSup_le'
modified theorem ciSup_of_empty
modified theorem ciSup_pos
modified theorem ciSup_subsingleton
modified theorem ciSup_unique
modified theorem iSup_disjointed
modified theorem iUnion_disjointed
modified theorem Filter.iInf_principal
modified theorem Filter.iSup_inf_principal
modified theorem Filter.iSup_join
modified theorem Filter.iSup_principal
modified theorem IsMaxOn.iSup_eq
modified theorem IsMinOn.iInf_eq
modified theorem Filter.iInf_le_liminf
modified theorem iSup_partialSups_eq
modified theorem LowerSet.iSup_Iic
modified theorem UpperSet.iInf_Ici
modified theorem Real.iInter_Iic_rat
modified theorem Real.iUnion_Iic_rat
modified theorem Cardinal.mk_iUnion_le
modified theorem Cardinal.mk_sUnion_le
modified theorem ENNReal.biInf_le_nhds
modified theorem ENNReal.iInf_mul_left'
modified theorem ENNReal.iInf_mul_right'
modified theorem Metric.iUnion_ball_nat
modified theorem Metric.iUnion_ball_nat_succ
modified theorem bsupr_limsup_dimH
modified theorem iSup_limsup_dimH
modified theorem CompactExhaustion.iUnion_eq
modified theorem iUnion_compactCovering
modified theorem iSup_nhds_le_uniformity
modified theorem Pi.uniformity