Why no explicit ContinuousWithinAt.continuousOn?

Stream: Is there code for X?

[Terence Tao]

I recently needed the following lemma which is immediate from the definition of `ContinuousOn':

import Mathlib

example [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h: ∀ x ∈ s, ContinuousWithinAt f s x) : ContinuousOn f s := by
  exact h

In analogy with docs#ContinuousAt.continuousOn or docs#ContinuousOn.continuousWithinAt, I would have expected this lemma to exist as ContinuousWithinAt.continuousOn, but this doesn't seem to be the case. I am wondering if this is a deliberate design decision? Are statements that are tautologically true from definition not usually explicitly stated as Mathlib lemmas?

[Yury G. Kudryashov]

Usually, the only reason to state something like this is to allow dot notation.

[Yury G. Kudryashov]

Unless you need a dot notation lemma, you can just use h whenever you need ContinuousOn f s.

[Yury G. Kudryashov]

Or add a type annotation to whatever have/obtain gave you this h.

[Yury G. Kudryashov]

I'm not sure why we need ContinuousOn.continuousWithinAt. I would never use it but probably someone @Sebastien Gouezel thinks that it's more readable (added in !3#2165).

[Terence Tao]

OK, but then this means that these sorts of obvious steps cannot be performed just from Mathlib searches, and one actually has to inspect the definition of terms such as ContinuousOn in order to proceed. I would have thought a more "object oriented" approach would be to turn these definitionally true statements into explicit methods, so was puzzled by the different philosophy espoused here.

[Yury G. Kudryashov]

As you can see, there are people with different tastes among maintainers. While I wouldn't use this lemma, I wouldn't object adding it to the library either.

[Terence Tao]

Well, all I know is that I spent fifteen minutes trying to search Mathlib for how to reduce from ContinuousOn to ContinuousWithinAt before finally looking at the definition of ContinuousOn to see that what I wanted was true by definition. I would have appreciated some hint that this is what I should have been doing in the first place, if this sort of method wasn't going to be put into Mathlib in the first place.

[Yury G. Kudryashov]

This is a good argument pro adding this method.

[Yury G. Kudryashov]

Indeed, https://loogle.lean-lang.org/?q=ContinuousOn%2C+ContinuousWithinAt returns one implication but doesn't show the definition.

[Yury G. Kudryashov]

Possibly, we should both add a lemma for the other implication (or an iff) and make loogle show the definition in cases like this one.

[Yury G. Kudryashov]

@Joachim Breitner :up: What do you think about it?

[Yury G. Kudryashov]

The idea is to match terms in the definition, not only type, for defs (not theorems).

[Yury G. Kudryashov]

@Terence Tao Generally, many parts of the library lack trivial lemmas because (a) it's easy to forget about these lemmas when you're writing API about a new definition; (b) we don't have formal coding style requirements + linters for this.

[Eric Wieser]

If instead of calling it ContinuousWithinAt.continuousOn we called it ContinuousOn.of_continuousWithinAt, then this would provide dot notation as (.of_continuousWithinAt h)

[Eric Wieser]

Of course this breaks that pattern set by most other lemmas

[Yury G. Kudryashov]

This wouldn't provide dot notation because of the way Lean 4 dels with .dot_lemma _: it intros everything it can before looking at the type of the target.

[Frédéric Dupuis]

I think lemmas like this should be in the library even though they're true by definition. I can also picture myself wasting time on this.

[Adam Topaz]

I assume exact? is unable to help in this case?

[Eric Wieser]

Yury G. Kudryashov said:

This wouldn't provide dot notation.

I'm referring to dot constructor notation, as opposed to the narrower Lean 3 meaning of dot notation.

[Yury G. Kudryashov]

Last time I checked, it doesn't work (EDIT: this is about dot notation, not exact?).

[Eric Wieser]

Yury G. Kudryashov said:

This wouldn't provide dot notation because of the way Lean 4 dels with .dot_lemma _: it intros everything it can before looking at the type of the target.

Oh, so the issue is that ContinuousOn is too reducible?

[Yury G. Kudryashov]

For cases like ContinuousOn.

[Yury G. Kudryashov]

Yes, it would work for a structure ContinuousOn.

[Adam Topaz]

In lean3 we had library_search! which was more aggressive than library_search with respect to reducibility. If we had such a exact?! then I would hope it would be able to find it.

[Terence Tao]

Adam Topaz said:

I assume exact? is unable to help in this case?

exact? works here. The problem was that because docs#ContinuousAt.continuousOn and docs#ContinuousOn.continuousWithinAt were already in the library, this strongly suggested that something like docs#ContinuousWithinAt.continuousOn was also in the library, so I spent most of my time looking for this using the various Mathlib search engines rather than trying other approaches such as exact?.

[Adam Topaz]

Ah I see.

[Yury G. Kudryashov]

I think that we should make loogle show this one way or another (add a lemma or change loogle).

[Adam Topaz]

Personally I tend to stay in the editor as much as possible, only opening a web browser as a last resort.

[Yury G. Kudryashov]

I use loogle a lot whenever I need a part of the library that I don't know well.

[Adam Topaz]

In any case, I’m addition to adding some declarations for this particular case, it seems that we also need to improve our various search engines (but we already knew that for a long time).

[Adam Topaz]

For example I think it would be reasonable if loogle was able to see through one layer of definitions with default reducibility.

[Yury G. Kudryashov]

Should it unfold 1 layer for defs only, or for theorems too?

[Sebastien Gouezel]

I'm a little bit late here, but I am strongly in favor of adding the lemma. Having a coherent and predictable library is IMHO a very important goal.

[Joachim Breitner]

@Adam Topaz , there is Loogle as a VSCode extension now, no need to reach for the browser any more!
https://marketplace.visualstudio.com/items?itemName=ShreyasSrinivas.loogle-lean

[Yaël Dillies]

I mean in that case surely the answer is to delete docs#ContinuousAt.continuousOn instead. This name is nonsense. There's no possible dot notation here.

[Yaël Dillies]

And if it hadn't been there, Terence Tao wouldn't have tried ContinuousWithinAt.continuousOn.

[Yaël Dillies]

At least rename the incriminated lemma to a name that makes sense with respect to the absence of dot notation, like continuousOn_of_forall_continuousAt. Then we can have continuousOn_iff_forall_continuousWithinAt for discoverability purposes.

[Eric Wieser]

Yury G. Kudryashov said:

Last time I checked, it doesn't work (EDIT: this is about dot notation, not exact?).

I think we should report this upstream; Lean shouldn't be introing here IMO. Then we can keep the existing lemma and add the new one with the .of name

[Yury G. Kudryashov]

I'm busy the next few days. Could you open an issue, please?

[Junyan Xu]

Yaël Dillies said:

At least rename the incriminated lemma to a name that makes sense with respect to the absence of dot notation, like continuousOn_of_forall_continuousAt. Then we can have continuousOn_iff_forall_continuousWithinAt for discoverability purposes.

I think normally definitional lemmas are simply called continuousOn_iff? Can we extend @[mk_iff] to generate such lemmas as well? (I tried and Lean says mk_iff only applies to inductive declarations.) By the way what happens when I rw [continuousOn]? Does Lean uses some equational lemma hidden somewhere, or is it implemented as an unfold?

[Yaël Dillies]

Yeah but the point here is that what lemma is definitional is non-obvious (and indeed it could well have been another one instead). rw [foo] uses the equational lemma generated for foo. It is explicitly not an unfold (and so in particular it works when foo is defined using well-founded recursion).

[Yury G. Kudryashov]

But loogle would find the continuousOn_iff lemma.