Topology.Bornology.Basic

Stream: mathlib4

[Jireh Loreaux]

This file is nearly done (mathlib4#1822), I just don't know how to handle the situation where we define a structure and want the argument to one of its data-carrying fields to be explicit. In Lean 3, this was handled with the [] syntax (see docs#bornology). In Lean 4, this notation is not supported. For non-data-carrying fields, we can handle this with the technique in docs4#Countable (versus docs#countable) as described in this thread, but for data-carrying fields this "duplication" trick seems like a bad idea (because of @[ext] or @[simps] lemmas at the very least). Suggestions or pushes welcome.

[Eric Wieser]

The solution for data carrying fields is I think to do the same thing, but define the ext lemma manually and a custom simps projection

[Jireh Loreaux]

I can't seem to get initialize_simps_projections to write a lemma about (cobounded α).sets instead of cobounded'.sets, where

class Bornology (α : Type _) where
  cobounded' : Filter α
  le_cofinite' : cobounded' ≤ cofinite

def Bornology.cobounded (α : Type _) [Bornology α] : Filter α := Bornology.cobounded'

initialize_simps_projections Bornology (cobounded' → cobounded)

Can someone help me out here?

[Eric Wieser]

IIRC you need to add a second def called Bornology.simps.cobounded in terms of the first def

[Jireh Loreaux]

I tried that before. While it does seem to register (by looking at the @[simps?] trace), it doesn't seem to have an effect on the .sets projection for Filter (this is a composite projection).

[Eric Wieser]

So [simps cobounded] works but [simps] by itself generates a lemma about cobounded'.sets?

[Floris van Doorn]

Do you want to generate e.g.

(Bornology.cobounded α).sets = { s | sᶜ ∈ B }

for Bornology.ofBounded? You can do that by adding

alias Bornology.cobounded ← Bornology.Simps.cobounded

initialize_simps_projections Bornology (cobounded' → cobounded)

As Eric said, you can use @[simps cobounded] to get an equality of filters (not recommended for something like Bornology.ofBounded).

If you also care about the name of the generated lemma (you don't want a trailing _sets in the lemma name), you can do something fancy like

def Bornology.custom_name (α : Type _) [Bornology α] : Set (Set α) := Bornology.cobounded'.sets

initialize_simps_projections Bornology (- cobounded', cobounded'_sets → custom_name)

this will generate e.g.

Bornology.ofBounded_custom_name: Bornology.cobounded'.sets = { s | sᶜ ∈ B }

[Jireh Loreaux]

My error was too stupid: I wrote Bornology.simps.cobounded not Bornology.Simps.cobounded :face_palm:

[Jireh Loreaux]

Thanks, this all works now.

[Eric Wieser]

The rule here is "it's a namespace, so it's capitalized"?

[Jireh Loreaux]

:shrug:

[Floris van Doorn]

I made this change because people (or mathport) wrote definitions with Simps capitalized. I must say this has also tripped me up. But notice that initialize_simps_projections? will tell you of all the custom projections it found, so that is a good way to check.

[Jireh Loreaux]

On a completely different note: in porting this file there were two times where I had to provide the Bornology type class argument to isBounded_def when used as a rewrite/simp lemma. In Lean 3 these were found automatically, and this seems like a regression. Search the file for porting note and you'll see them.