Sebastien Gouezel

Results 27 comments of Sebastien Gouezel

feat(analysis/convex/topology): minimize import

bors d+

apply_instance and reducibility flag

I just stumbled on the same issue (with pretty complicated pi types, again). Is there hope that https://github.com/leanprover-community/lean/pull/300 could change something here? (It involves pi types and instance search and...

apply_instance and reducibility flag

Just checked on Lean 3.16, and the behavior is the same. I guess you're right, this is a (complicated) unification problem.

feat(analysis/complex/open_mapping): the open mapping thm for holomorphic functions

That's really cool! For each lemma whose proof is longer than 10 lines, could you please add a docstring explaning the content of the result, and a comment at the...

chore(analysis/inner_product_space/basic): remove `bilin_form_of_real_inner`

Can you merge master and fix the build? bors d+ Thanks!

feat(analysis/inner_product_space/two_dim): the case of `ℂ`

bors r+

feat(analysis/bounded_variation): functions of bounded variation are ae differentiable

bors r+

feat(measure_theory/integral/circle_transform): Circle transform results pt2

Could you split this PR into two, one doing the renaming, and the other one adding the new content? This would make it easier to review.

refactor(tactic/wlog): simplify and speed up `wlog`

bors r- Can you merge master and fix the build? bors d+

feat(topology/metric_space/infsep): Add "infimum separation".

LGTM, thanks! You can merge it once CI is happy. bors d+