Countable union property to finite union property

Stream: new members

[Josha Dekker]

I'm stuck trying to prove the following; is there a standard theorem for this? (It seems relatively basic, so I'd guess so). The math reasoning would be : extend a finite set S to an infinite set S by appending the empty-set infinitely often; by 'he' we can then use the hypothesis hcountable_union.

universe u
variable {X : Type u}

theorem finite_from_union {p : Set X → Prop} (he : p ∅) (hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃ s, s)) : ∀ (S : Set (Set X)), S.Finite → (∀ s ∈ S, p s) → p (⋃ s, s))

[Josha Dekker]

(deleted)

[Kevin Buzzard]

docs#Set.Countable

[Kevin Buzzard]

Looks to me like finite sets are countable in lean so you don't need to do any extending.

[Kevin Buzzard]

So just use docs#Set.Finite.countable (found with moogle.ai)

[Josha Dekker]

Excellent, thank you! I tried Google, but somehow must've overlooked this one!

[Kevin Buzzard]

(now at a computer)

import Mathlib
universe u
variable {X : Type u}

theorem finite_from_union {p : Set X → Prop} (he : p ∅)
    (hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃ s, s)) :
    ∀ (S : Set (Set X)), S.Finite → (∀ s ∈ S, p s) → p (⋃ s, s) := by
  peel hcountable_union with hS S
  intro h
  apply hS
  exact Set.Finite.countable h

[Josha Dekker]

Thank you, that works neatly!