mathlib3
feat(analysis/convex): interiors/closures of convex sets are convex in a tvs
#1781
Merged
Merged
feat(analysis/convex): interiors/closures of convex sets are convex in a tvs #1781
mergify
merged
16 commits into
master
from
convex-lem
feat(topology/algebra/module): scalar multiplication homeomorphisms
f25bb949
feat(topology/algebra/module): more lemmas
d74444cf
feat(analysis/convex): interior of convex set is convex in a tvs
adc9e9b7
feat(analysis/convex): extract lemma
7594ac2c
feat(analysis/convex): closure of a convext set is convex
6f72cd10
style(analysis/convex): place lemmas at reasonable locations
17a6fdca
Merge branch 'master' of https://github.com/leanprover-community/math…
99bc3663
jcommelin
commented
on 2019-12-05
sgouezel
commented
on 2019-12-05
sgouezel
commented
on 2019-12-05
style(topology/algebra/module): fix bracketing style
b0249b31
Merge branch 'master' of https://github.com/leanprover-community/math…
aca94d57
feat(analysis/convex): introduce `smul_set` and `pointwise_mul`
39396f0d
feat(algebra/pointwise): lemmas for `smul_set`
7846a1a7
Merge branch 'master' of https://github.com/leanprover-community/math…
e2ae02cf
doc(algebra/pointwise): add docstrings
13914c2b
sgouezel
commented
on 2019-12-08
doc(algebra/pointwise): add global docstring
b94fa599
Merge branch 'master' of https://github.com/leanprover-community/math…
6dfaefd8
sgouezel
approved these changes
on 2019-12-10
docs(algebra/pointwise): amend global docstring
fe860359
Login to write a write a comment.
Login via GitHub