mathlib
4f3e99a6 - feat(topology/algebra): range of `coe_fn : (M₁ →ₛₗ[σ] M₂) → (M₁ → M₂)` is closed (#11105)

Commit

3 years ago

feat(topology/algebra): range of `coe_fn : (M₁ →ₛₗ[σ] M₂) → (M₁ → M₂)` is closed (#11105) Motivated by #9862

Author

urkud

Parents