singleton type

Stream: new members

[Laurent Bartholdi]

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]

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

[Eric Wieser]

Does this still happen in lean 4?

[Laurent Bartholdi]

Sorry, I should have said that this is in lean3

[Laurent Bartholdi]

Indeed,

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

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

[Jireh Loreaux]

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

[Floris van Doorn]

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]

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 ...)