Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.eq_top_of_nonempty_interior

Modification history

2020-07-21 01:55
src/topology/algebra/module.lean
refactor(topology/algebra/monoid): changed topological_monoid into has_continuous_mul (#3481)
Deleted submodule.eq_top_of_nonempty_interiorView on Github →
2020-07-19 21:18
src/analysis/normed_space/basic.lean
refactor(order/filter/basic): add class `filter.ne_bot` (#3454) …
Modified submodule.eq_top_of_nonempty_interiorView on Github →
2020-05-19 09:58
src/analysis/normed_space/basic.lean
feat(analysis/normed_space): interior of `closed_ball` etc (#2723) …
Modified submodule.eq_top_of_nonempty_interiorView on Github →
2020-02-19 21:46
src/analysis/normed_space/basic.lean
refactor(analysis/calculus/tangent_cone): split a proof into parts (#2013) …
Added submodule.eq_top_of_nonempty_interiorView on Github →