Zulip Chat Archive

Stream: new members

Topic: singleton type

Laurent Bartholdi (Jun 14 2023 at 13:39):

A newbie question:

definition has_no_isolated_points (α : Type*) [topological_space α] := x : α, ¬is_open ({x} : set α)
definition has_no_isolated_points' (α : Type*) [topological_space α] := x : α, ¬is_open {x}

The first definition works, the second does not. I saw on another thread that {x} has different meanings, e.g. as a set and as a finset; but surely lean knows that is_open requires a set, so why doesn't the type system infer it?

Riccardo Brasca (Jun 14 2023 at 13:40):

With set this unfortunately often happens, Lean needs a little help

Eric Wieser (Jun 14 2023 at 13:40):

Does this still happen in lean 4?

Laurent Bartholdi (Jun 14 2023 at 13:41):

Sorry, I should have said that this is in lean3

Laurent Bartholdi (Jun 14 2023 at 13:45):


def HasNoIsolatedPoint (α : Type) [TopologicalSpace α] := x : α, ¬IsOpen {x}

works like a charm. A problem that will disappear on its own, then :)

Jireh Loreaux (Jun 14 2023 at 16:08):

Eric, no, I think not because of default instances.

Floris van Doorn (Jun 15 2023 at 15:50):

Laurent Bartholdi said:

why doesn't the type system infer it?

I think the problem is that is_open requires a set in some unknown type, but it's not a priori clear that this type is α. Unfortunately the meaning of {x} will only be figured out once the exact type of it is known, so set ?m is not good enough, it needs the help that it has type set α. This is indeed unfortunate.

Kevin Buzzard (Jun 15 2023 at 21:10):

This was also an irritating thing in lean 3 (although IIRC it didn't happen back in 2017 before we started to get interested in getting set notation to work for finsets too ...)

Last updated: Dec 20 2023 at 11:08 UTC