Commit 2024-04-10 06:01 6201c942

View on Github →

chore(Data/Set/Function): add sections to group related material (#11675)

  • delay on open statement until actually needed
  • note that two lemmas seem mis-placed
  • use some namespaces

Estimated changes

modified theorem Set.InvOn.bijOn
modified theorem Set.InvOn.comp
modified theorem Set.InvOn.mono
modified theorem Set.InvOn.symm
modified theorem Set.LeftInvOn.comp
modified theorem Set.LeftInvOn.congr_left
modified theorem Set.LeftInvOn.congr_right
modified theorem Set.LeftInvOn.eq
modified theorem Set.LeftInvOn.eqOn
modified theorem Set.LeftInvOn.image_image'
modified theorem Set.LeftInvOn.image_image
modified theorem Set.LeftInvOn.image_inter'
modified theorem Set.LeftInvOn.image_inter
modified theorem Set.LeftInvOn.injOn
modified theorem Set.LeftInvOn.mapsTo
modified theorem Set.LeftInvOn.mono
modified theorem Set.LeftInvOn.surjOn
modified theorem Set.RightInvOn.comp
modified theorem Set.RightInvOn.congr_left
modified theorem Set.RightInvOn.congr_right
modified theorem Set.RightInvOn.eq
modified theorem Set.RightInvOn.eqOn
modified theorem Set.RightInvOn.mapsTo
modified theorem Set.RightInvOn.mono
modified theorem Set.RightInvOn.surjOn
modified theorem Set.invOn_id
modified theorem Set.leftInvOn_id
modified theorem Set.rightInvOn_id