mathlib3
7f541b4e - feat(topology/continuous_function): on a subsingleton X, there is only one subalgebra R C(X,R) (#7247)

Commit

4 years ago

feat(topology/continuous_function): on a subsingleton X, there is only one subalgebra R C(X,R) (#7247) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

cab0481e

mathlib3 7f541b4e - feat(topology/continuous_function): on a subsingleton X, there is only one subalgebra R C(X,R) (#7247)

mathlib3
7f541b4e - feat(topology/continuous_function): on a subsingleton X, there is only one subalgebra R C(X,R) (#7247)