minLayer naming

Stream: Carleson

[Joachim Breitner]

Jeremy Tan said:

And linked my minLayer to Breitner's height

Thanks for connecting and cleaning up! The minLayer is the same thing that I proposed to name withHeight, right? Naming questions become more relevant only when and if this goes to mathlib, but when then happens I suggest to consider whether something alluding to “iterated minimals“ or “height” is the appropriate name.

At least to me “elements of height n” seems the more basic notion here, so maybe

A.minLayer n = {x | ∃ hx : x ∈ A, height (⟨x, hx⟩ : A) = n}

(possibly named something related to height) should be the definition (and influence the name), and the fact that it can be defined recursively using minimals is just one interesting property of that definition.

But not pressing, this can wait until and if upstreaming happens.

In any case, I’ll focus on upstreaming stuff up to height.