Finite union of Singletons is finite. How to show?

Stream: new members

[Kent Van Vels]

I am trying to show that the finite union of Singleton sets is finite and I haven't been able to make progress. Here is my MWE. I am also unclear of the the "type" the union in my MWE. None of iUnion, sUion, biUnion, seem to fit.

import Mathlib.Tactic
open Set Finset

variable {X : Type*}
variable (tFinite : Finset X)

theorem  h4 :
Set.Finite (⋃ x ∈ tFinite, Set.singleton x) := by sorry

Does this type of Union have a name? Lean seems to complain if I call it an sUnion, or an iUnion.

I did try use #Set.Finite.sUnion and #Set.Finite.iUnion but I hit deads ends.

I appreciate any help.

[Kent Van Vels]

VS code is telling me that it is an iUnion, and I see how that makes sense.

[Kevin Buzzard]

I don't really understand the naming convention. sUnion is union of a set of sets, i.e. you need a term of type Set (Set X). iUnion is a union over a type. The closest I can find is biUnion which seems to be over a set, and you can force progress with convert:

import Mathlib
open Set Finset

variable {X : Type*}
variable (tFinite : Finset X)

theorem  h4 : Set.Finite (⋃ x ∈ tFinite, Set.singleton x) := by
  convert Finite.biUnion (s := (tFinite : Set X)) ?_ ?_
  · exact finite_toSet tFinite
  · intros
    -- ⊢ (Set.singleton i✝).Finite
    exact? -- how can we not have this??

[Ruben Van de Velde]

It helps if you write singletons "correctly" as {x}

[Ruben Van de Velde]

Then apply? immediately finds exact toFinite (⋃ x ∈ tFinite, {x})

[Kevin Buzzard]

One thing which is weird about your statement is that you're mixing two different notions of finiteness: you have Finset X as a hypothesis but Set.Finite as a conclusion. Maybe you want to choose which one you want to use? Here's a solution with Set.Finite:

import Mathlib
open Set Finset

variable {X : Type*}
variable {t : Set X} (htfinite : Set.Finite t)

include htfinite in
theorem  h4 : Set.Finite (⋃ x ∈ t, {x}) := by
  apply Finite.biUnion htfinite
  intro i hi
  exact finite_singleton i

[Bjørn Kjos-Hanssen]

Another solution

import Mathlib.Tactic
open Set Finset

variable {X : Type*}
variable (s : Finset X)

theorem  h4 :
Set.Finite (⋃ x ∈ s, Set.singleton x) :=
  Finite.biUnion' (Finite.of_fintype { x // x ∈ s }) fun _ _ => Subsingleton.finite <| subsingleton_of_subset_singleton fun ⦃_⦄ => congrArg fun ⦃a⦄ => a

[Kent Van Vels]

I am trying to show compactness (the open cover defn) in a metric space implies sequential compactness and I just copied the output of #IsCompact.elim_finite_subcover. (how do I make that a link?) So that is where I got the Finset stuff from.

I am not done yet, so I might be able to switch to the other notion of finiteness.

I did switch to the curly bracket notation for singletons and apply? gave me an exact term. I am currently trying to understand that now.

For anyone's information the following works.

import Mathlib.Tactic
open Set Finset

variable {X : Type*}
variable (tFinite : Finset X)

--#check  (⋃ x ∈ tFinite, Set.singleton x)

theorem  h4 : Finite (⋃ x ∈ tFinite,  Set.singleton x) := by
  exact Finite.Set.finite_biUnion'' (Membership.mem tFinite) singleton

Thanks for the help, @Kevin Buzzard @Ruben Van de Velde.

[Kent Van Vels]

Also, thank you @Bjørn Kjos-Hanssen ☀️ I appreciate it.

[Daniel Weber]

To make a link you need to add docs, e.g. docs#Nat