Stream: new members
Topic: RFC: operator norm
Jan-David Salchow (Dec 28 2018 at 22:36):
I've been playing with the space of bounded linear maps between normed space, see https://github.com/jdsalchow/mathlib/blob/calculus/analysis/functional/operator_norm.lean
Before splitting this up into smaller pieces and creating a PR, I thought I better ask for comments. So, comments anybody?
Kevin Buzzard (Dec 28 2018 at 23:52):
local attribute[instance] classical.prop_decidable -- people often go for
local attribute [instance, priority 0] classical.prop_decidable nowadays because it is less likely to break proofs that actually rely on decidability. This might well not be an issue in this code though.
Jan-David Salchow (Dec 29 2018 at 09:59):
Is there a way to forget a local attribute when it's not needed anymore?
Chris Hughes (Dec 29 2018 at 10:02):
put it inside a section
Last updated: May 11 2021 at 21:10 UTC