Set.finite

This file handles a simple definition for when a set is considered finite, namely when there exists a list that contains the same elements.

def Set.finite {α : Type u_1} (X : Set α) : Prop

A set is finite if there is a list with the same elements. We also enforce this list to be free of duplicates right now but this might change in the future.

Equations

• X.finite = ∃ (l : List α), l.Nodup ∧ ∀ (e : α), e ∈ l ↔ e ∈ X

theorem Set.finite_of_list_with_same_elements {α : Type u_1} [DecidableEq α] {X : Set α} (l : List α) (same_elements : ∀ (e : α), e ∈ l ↔ e ∈ X) : X.finite

To show that a Set is finite, it is enough to give a list with the same elements not caring about duplicates. Duplicates are removed using List.eraseDupsKeepRight internally.

theorem Set.finite_of_subset_finite {α : Type u_1} [DecidableEq α] {a b : Set α} (fin : b.finite) : a ⊆ b → a.finite

Subsets of finite sets are finite.

theorem Set.union_finite_of_both_finite {α : Type u_1} [DecidableEq α] {a b : Set α} (fin_a : a.finite) (fin_b : b.finite) : (a ∪ b).finite

Unions of finite sets are finite.

theorem List.finite_toSet {α : Type u_1} [DecidableEq α] (l : List α) : l.toSet.finite

Sets obtained from lists are finite.