α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
hsc : Set.Finite (sᶜ)
⊢ Set.Finite (s ∪ sᶜ)
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
hsc : Set.Finite (sᶜ)
⊢ Finite α
rw [← finite_univ_iff, ← union_compl_self s]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
hs : Set.Finite s
hsc : Set.Finite (sᶜ)
⊢ Set.Finite (s ∪ sᶜ)
exact hs.union hsc