mathlib3
8f5303ae - refactor(topology/connected): drop `local attribute [instance] connected_component_setoid` (#11365)

Commit

3 years ago

refactor(topology/connected): drop `local attribute [instance] connected_component_setoid` (#11365) Add a coercion from `X` to `connected_components X` instead.

Author

urkud

Parents

c1c0fa4a

mathlib3 8f5303ae - refactor(topology/connected): drop `local attribute [instance] connected_component_setoid` (#11365)

mathlib3
8f5303ae - refactor(topology/connected): drop `local attribute [instance] connected_component_setoid` (#11365)