TC normal form

Stream: maths

[Yury G. Kudryashov]

Sometimes I use docs#filter.ne_bot to express notions that possibly deserve a dedicated typeclass. What do you think about the following two cases?

[Yury G. Kudryashov]

/poll Normal form for “x is not an isolated point”
ne_bot (𝓝[{x}ᶜ] x)
create new TC non_isolated_pt

[Yury G. Kudryashov]

/poll Normal form for “non-compact space”
ne_bot (cocompact α)
is_empty (compact_space α)
add new TC noncompact_space

[Yury G. Kudryashov]

Pros of new TCs:

• more readable code;
• no false negatives for the "priority" linter.

[Patrick Massot]

If we really need this to be inferred by type class resolution then I think non_compact_space is the only readable option

[Yury G. Kudryashov]

If we infer this by type class resolution, then we can make an instance for alexandroff.connected_space.