Finding and importing notation ℕ

Stream: mathlib4

[Bob Rubbens]

Hi everyone,

I'm trying to use the notation ℕ for natural numbers. I found through a random topic about mathlib that the following import does the trick:

import Mathlib.Data.Real.Basic

I've tried searching for "ℕ" on the auto generated mathlib docs, but that only yielded some unrelated definitions (I think). Any time I click on the type "ℕ" in the mathlib documentation, I am redirected to the definition of Nat in the standard library.

My questions are:

1. What is the precise import I need to get the "ℕ" notation to work? I think the import I have now also imports a bunch of Real stuff, which is fine, but I'm curious about where the exact definition of this notation is.
2. How could I conceivably have found this notation on my own. Are there any other sources or search methods I should consider when I have questions like this?

[Kevin Buzzard]

If I right-click on ℕ and then choose "go to declaration" I see that the notation is defined in Mathlib.Data.Nat.Notation.

[Damiano Testa]

You can also do this:

import Mathlib

/--
info: Found 4 uses among 2394 syntax declarations
In `Mathlib.Data.ENat.Defs`:
  «termℕ∞»: 'ℕ∞'

In `Mathlib.Data.Nat.Notation`:
  termℕ: 'ℕ'

In `Mathlib.Data.PNat.Notation`:
  «termℕ+»: 'ℕ+'

In `Mathlib.Topology.Category.LightProfinite.Sequence`:
  LightProfinite.«termℕ∪{∞}»: 'ℕ∪{∞}'
-/
#guard_msgs in
#find_syntax "ℕ"

[Violeta Hernández]

we have notation ℕ∪{∞}? yikes

[Kenny Lau]

i'm in the camp of "as much notation as possible"

[Alex Meiburg]

I am too, but that is not what I would have expected ℕ∪{∞} to mean..

[Aaron Liu]

it's ENat, as a bundled second countable totally disconnected compact hausdorff topological space

[Dagur Asgeirsson]

It's specialized notation for condensed mathematics, living inside the LightProfinite namespace :shrug:

[Floris van Doorn]

Kenny Lau said:

i'm in the camp of "as much notation as possible"

Agreed, on the condition that it is scoped.

[Kenny Lau]

Floris van Doorn said:

Agreed, on the condition that it is scoped.

Agreed, on the condition that docgen opens all scoped notations, seeing TensorProduct and CategoryStruct.comp on the docs doesn't really help anyone