Continuity lemmas and @[continuity]

Stream: general

[Eric Wieser]

What's the recommendation for use of @[continuity] in light of the "continuity lemma statement" library note? Which of docs#real.continuous_sqrt and docs#continuous.sqrt should be tagged with @[continuity]?

[Eric Wieser]

Some other examples:

traditional	library note
docs#real.continuous_exp (attribute)	docs#continuous.exp (no attribute)
docs#real.continuous_cos (attribute)	docs#continuous.cos (doesn't exist)
docs#has_continuous_neg.continuous_neg (no attribute)	docs#continuous.neg (attribute)

[Eric Wieser]

Judging by the implementation of continuity it seems like it is able to handle the "traditional" version that is hard to use with apply

[Eric Wieser]

run_cmd do
  x ← attribute.get_instances `continuity,
  let (x1, x2) := x.partition (λ x, (`continuous).is_prefix_of x),
  tactic.trace x1.length,
  tactic.trace x2.length

suggests we have equal numbers in each category

[Eric Wieser]

@Floris van Doorn, I seem to remember you wrote the library note; do you have any opinions here?

[Floris van Doorn]

The library note is meant to describe the correct design for human use. I don't know the inner details of the continuity tactic to know what is most convenient for it. If both of them work, I expect it doesn't matter that much for unary functions. For binary or n-ary functions I expect that we want the @[continuity] attribute on the lemmas that follow the library note, since this is the case where the elaborator will get confused if you don't follow the library note.