Commit 2023-06-30 01:46 4d4f0f25

View on Github →

fix: change compl precedence (#5586)

Estimated changes

modified theorem ofBoolAlg_compl
modified theorem IsIdempotentElem.coe_compl
modified theorem Set.compl_star
modified theorem Function.compl_mulSupport
modified theorem contDiffOn_inv
modified theorem eqOn_dslope_slope
modified theorem IsLprojection.coe_compl
modified theorem IsLprojection.compl_mul
modified theorem nonunits.subset_compl_ball
modified theorem Real.continuousOn_log
modified theorem Real.contDiffOn_log
modified theorem Real.differentiableOn_log
modified theorem Real.contDiffOn_arccos
modified theorem Real.contDiffOn_arcsin
modified theorem Finset.insert_inj_on
modified theorem Finset.coe_compl
modified theorem Finset.compl_erase
modified theorem Finset.compl_insert
modified theorem Fintype.card_compl_set
modified theorem Set.BijOn.compl
modified theorem Set.MapsTo.mem_iff
modified theorem Set.MapsTo.surjOn_compl
modified theorem Set.SurjOn.mapsTo_compl
modified theorem Set.piecewise_eqOn_compl
modified theorem Set.compl_image_set_of
modified theorem Set.compl_range_inl
modified theorem Set.compl_range_inr
modified theorem Set.compl_range_some
modified theorem Set.compl_Ici
modified theorem Set.compl_Iic
modified theorem Set.compl_Iio
modified theorem Set.compl_Ioi
modified theorem Set.compl_iInter
modified theorem Set.compl_iInter₂
modified theorem Set.compl_iUnion
modified theorem Set.compl_iUnion₂
modified theorem Set.compl_inv
modified theorem Set.offDiag_univ
modified theorem Set.pi_inter_compl
modified theorem MeasurableSet.coe_compl
modified theorem MeasurableSet.compl_iff
modified theorem MeasureTheory.measure_compl
modified theorem MeasureTheory.ae_eq_univ
modified theorem MeasureTheory.mem_ae_iff
modified theorem Set.Definable.compl
modified theorem disjoint_compl_left_iff
modified theorem disjoint_compl_right_iff
modified theorem isCompl_compl
modified theorem Set.compl_cIcc
modified theorem Set.compl_cIoo
modified theorem compl_iInf
modified theorem compl_iSup
modified theorem compl_sInf'
modified theorem compl_sInf
modified theorem compl_sSup'
modified theorem compl_sSup
modified theorem disjointed_eq_inf_compl
modified theorem disjointed_eq_inter_compl
modified theorem Filter.isCompl_principal
modified theorem Filter.mem_of_eq_bot
modified theorem LE.le.disjoint_compl_left
modified theorem LE.le.disjoint_compl_right
modified theorem disjoint_compl_left
modified theorem disjoint_compl_right
modified theorem ofDual_compl
modified theorem ofDual_hnot
modified theorem toDual_compl
modified theorem toDual_hnot
modified theorem map_compl
modified theorem Heyting.Regular.coe_compl
modified theorem Heyting.isRegular_compl
modified theorem map_compl'
modified theorem Filter.liminf_compl
modified theorem Filter.limsup_compl
modified theorem IsLowerSet.compl
modified theorem IsUpperSet.compl
modified theorem LowerSet.coe_compl
modified theorem UpperSet.coe_compl
modified theorem isLowerSet_compl
modified theorem isUpperSet_compl
modified theorem continuousOn_inv₀
modified theorem continuousOn_zpow₀
modified theorem Dense.interior_compl
modified theorem acc_iff_cluster
modified theorem closure_compl
modified theorem closure_compl_singleton
modified theorem frontier_compl
modified theorem interior_compl
modified theorem isClosed_compl_iff
modified theorem isOpen_compl_iff
modified theorem OnePoint.compl_range_coe
modified theorem Set.Countable.isGδ_compl
modified theorem Set.Finite.isGδ_compl
modified theorem Rat.dense_compl_compact
modified theorem IsClopen.compl
modified theorem isClopen_compl_iff