Finite set is union of singletons

Stream: Is there code for X?

[Riyaz Ahuja]

Hi! It seems really intuitively true that given a set A: Set X and hA: Set.Finite A, then we can write A as the finite union of singletons of each of its elements. However, I haven't been able to find a direct way to cite this fact.

I tried to convert A to a finset and then convert that to a list via (Set.Finite.toFinset hA).toList, but I'm not sure how to use that to show that ∃U:Fin (List.length list_A) → Set X, A = ⋃ i : Fin (List.length list_A), U i. It feels like there should be a way easier way to do this than all these conversions. Thanks!

[Kevin Buzzard]

Instead of asking a maths question in words, can you restate your question in Lean code with a sorry? For me there are several ways to say "I am a finite union of singletons of my elements", and every set is a union of the singletons of its elements, finite or not. So in some sense your question is not precise until you write it in code.

[Ruben Van de Velde]

It also feels like you have a #xy question here. Why do you want to write this set as a union of singletons?

[Riyaz Ahuja]

Thats a fair point. I'm trying to show that for MetricSpace X, if all x:X are not isolated, then all finite subsets of X are nowhere dense. Formally:

def NowhereDense (A: Set X) : Prop :=
  interior (closure (A)) = ∅

def limit_point (x: X) : Prop :=
∀ ε > 0, ∃ y : X, y ≠ x ∧ dist y x < ε

def isolated_point (x : X) : Prop := ¬(limit_point x)

lemma no_isolated_imp_finite_nowhere_dense (h: (∀x : X, ¬isolated_point x))
: ∀ A:Set X, Set.Finite A → NowhereDense A := by sorry

To do this, I showed that ∀ x: X, IsOpen {x} ↔ isolated_point x, and now all I need to do to essentially finish the proof is to show that A = ⋃ x:A , {x}. Then I can just use the properties and definitions of nowhere dense sets that I've already shown (finite union, etc) to finish the proof. Thanks again.

[Ruben Van de Velde]

There's docs#Set.iUnion_of_singleton