/bourbaki

Implementation in Lean4 of Bourbaki's "Éléments de mathématiques"

Primary LanguageLean

Bourbaki

Note on function naming

This code globally follows some of Mathlib4 conventions, namely

  • '' for image of a set
  • -1' for preimage of a set