Commit 2022-12-15 04:45 fd6ea186

View on Github →

feat: port Data.Set.Function (#1035) mathlib3 SHA: 198161d833f2c01498c39c266b0b3dbe2c7a8c07 porting notes:

  1. There are just a few declarations that need fixing still
  2. This was mostly fine, primarily tedious. One place I had to give an ugly workaround to avoid using lift since we don't have that yet.

Estimated changes

added theorem AntitoneOn.congr
added theorem AntitoneOn.mono
added theorem Function.insert_injOn
added theorem Function.invFunOn_eq
added theorem Function.invFunOn_mem
added theorem Function.invFunOn_neg
added theorem Function.invFunOn_pos
added theorem MonotoneOn.congr
added theorem MonotoneOn.mono
added theorem Set.BijOn.bijective
added theorem Set.BijOn.comp
added theorem Set.BijOn.compl
added theorem Set.BijOn.congr
added theorem Set.BijOn.image_eq
added theorem Set.BijOn.injOn
added theorem Set.BijOn.inter
added theorem Set.BijOn.inter_mapsTo
added theorem Set.BijOn.mapsTo
added theorem Set.BijOn.mk
added theorem Set.BijOn.subset_range
added theorem Set.BijOn.surjOn
added theorem Set.BijOn.union
added def Set.BijOn
added theorem Set.EqOn.bijOn_iff
added theorem Set.EqOn.cancel_left
added theorem Set.EqOn.cancel_right
added theorem Set.EqOn.comp_left
added theorem Set.EqOn.comp_right
added theorem Set.EqOn.image_eq
added theorem Set.EqOn.injOn_iff
added theorem Set.EqOn.mapsTo_iff
added theorem Set.EqOn.mono
added theorem Set.EqOn.piecewise_ite
added theorem Set.EqOn.surjOn_iff
added theorem Set.EqOn.symm
added theorem Set.EqOn.trans
added theorem Set.EqOn.union
added def Set.EqOn
added theorem Set.InjOn.bijOn_image
added theorem Set.InjOn.cancel_left
added theorem Set.InjOn.comp
added theorem Set.InjOn.congr
added theorem Set.InjOn.eq_iff
added theorem Set.InjOn.mono
added theorem Set.InjOn.ne_iff
added def Set.InjOn
added theorem Set.InvOn.bijOn
added theorem Set.InvOn.mono
added theorem Set.InvOn.symm
added def Set.InvOn
added theorem Set.LeftInvOn.comp
added theorem Set.LeftInvOn.eq
added theorem Set.LeftInvOn.eqOn
added theorem Set.LeftInvOn.injOn
added theorem Set.LeftInvOn.mapsTo
added theorem Set.LeftInvOn.mono
added theorem Set.LeftInvOn.surjOn
added def Set.LeftInvOn
added theorem Set.MapsTo.comp
added theorem Set.MapsTo.congr
added theorem Set.MapsTo.inter
added theorem Set.MapsTo.inter_bijOn
added theorem Set.MapsTo.inter_inter
added theorem Set.MapsTo.iterate
added theorem Set.MapsTo.mem_iff
added theorem Set.MapsTo.mono
added theorem Set.MapsTo.mono_left
added theorem Set.MapsTo.mono_right
added theorem Set.MapsTo.union
added theorem Set.MapsTo.union_union
added def Set.MapsTo
added theorem Set.RightInvOn.comp
added theorem Set.RightInvOn.eq
added theorem Set.RightInvOn.eqOn
added theorem Set.RightInvOn.mapsTo
added theorem Set.RightInvOn.mono
added theorem Set.RightInvOn.surjOn
added def Set.RightInvOn
added theorem Set.Subsingleton.injOn
added theorem Set.SurjOn.comp
added theorem Set.SurjOn.congr
added theorem Set.SurjOn.inter
added theorem Set.SurjOn.inter_inter
added theorem Set.SurjOn.mono
added theorem Set.SurjOn.union
added theorem Set.SurjOn.union_union
added def Set.SurjOn
added theorem Set.apply_piecewise
added theorem Set.apply_piecewise₂
added theorem Set.bijOn_empty
added def Set.codRestrict
added theorem Set.eqOn_comm
added theorem Set.eqOn_empty
added theorem Set.eqOn_piecewise
added theorem Set.eqOn_range
added theorem Set.eqOn_refl
added theorem Set.eqOn_union
added theorem Set.eq_restrict_iff
added theorem Set.image_restrict
added theorem Set.injOn_empty
added theorem Set.injOn_insert
added theorem Set.injOn_of_injective
added theorem Set.injOn_preimage
added theorem Set.injOn_singleton
added theorem Set.injOn_union
added theorem Set.le_piecewise
added theorem Set.mapsTo'
added theorem Set.mapsTo_empty
added theorem Set.mapsTo_id
added theorem Set.mapsTo_image
added theorem Set.mapsTo_inter
added theorem Set.mapsTo_preimage
added theorem Set.mapsTo_range
added theorem Set.mapsTo_singleton
added theorem Set.mapsTo_union
added theorem Set.mapsTo_univ
added theorem Set.maps_image_to
added theorem Set.maps_range_to
added theorem Set.maps_univ_to
added theorem Set.pi_piecewise
added theorem Set.piecewise_compl
added theorem Set.piecewise_empty
added theorem Set.piecewise_eqOn
added theorem Set.piecewise_insert
added theorem Set.piecewise_le
added theorem Set.piecewise_mem_pi
added theorem Set.piecewise_op
added theorem Set.piecewise_op₂
added theorem Set.piecewise_preimage
added theorem Set.piecewise_same
added theorem Set.piecewise_univ
added theorem Set.range_extend
added theorem Set.range_piecewise
added theorem Set.range_restrict
added def Set.restrict
added theorem Set.restrict_apply
added theorem Set.restrict_dite
added theorem Set.restrict_eq
added theorem Set.restrict_eq_iff
added theorem Set.restrict_ite
added theorem Set.restrict_ite_compl
added theorem Set.restrict_piecewise
added theorem Set.surjOn_empty
added theorem Set.surjOn_image
added theorem Set.univ_pi_piecewise
added theorem StrictAntiOn.comp
added theorem StrictAntiOn.congr
added theorem StrictAntiOn.injOn
added theorem StrictAntiOn.mono
added theorem StrictMono.codRestrict
added theorem StrictMonoOn.comp
added theorem StrictMonoOn.congr
added theorem StrictMonoOn.injOn
added theorem StrictMonoOn.mono
added theorem strictMono_restrict