mathlib

mathlib copied to clipboard

---

but I can do without if it seems too specialized.

I would lean towards saying it does; Let's wait till the other PRs #15541 are blocked by are resolved to decide.

I'd propose making this more lightweight by getting rid of the definition partial_span and just stating the lemma partial_span_dense in terms of ⨆ J : finset ι, span 𝕜 (J.image b : set E). The lemma partial_span_mono can probably also go and be replaced by an earlier lemma, a version span_monotone of span_mono which is actually expressed in terms of monotone; then the whole partial_span_mono is just (span_monotone 𝕜 E).comp (finset.image_mono b) and doesn't need to exist stand-alone.

@eric-wieser are you ok with this plan?

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests