leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: preimage


Patrick Massot (Jan 25 2019 at 22:02):

Why don't we use infix ` ⁻' `:80 := preimage?

Patrick Massot (Jan 25 2019 at 22:16):

Actually I may use notation f`⁻¹(`A`)` := f ⁻¹' A with my students

Mario Carneiro (Jan 25 2019 at 22:43):

it's a combination of ⁻¹ and the image operator ''

Mario Carneiro (Jan 25 2019 at 22:43):

⁻' is usable but possibly a bit obfuscatory


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll