def Set (α : Type u) : Type u

Equations

• Set α = (α → Prop)

instance instEmptyCollectionSet {α : Type u_1} : EmptyCollection (Set α)

Equations

• instEmptyCollectionSet = { emptyCollection := fun (x : α) => False }

instance instMembershipSet {α : Type u_1} : Membership α (Set α)

Equations

• instMembershipSet = { mem := fun (S : Set α) (a : α) => S a }

instance instUnionSet {α : Type u_1} : Union (Set α)

Equations

• instUnionSet = { union := fun (A B : Set α) (e : α) => e ∈ A ∨ e ∈ B }

instance instInterSet {α : Type u_1} : Inter (Set α)

Equations

• instInterSet = { inter := fun (A B : Set α) (e : α) => e ∈ A ∧ e ∈ B }

instance instHasSubsetSet {α : Type u_1} : HasSubset (Set α)

Equations

• instHasSubsetSet = { Subset := fun (A B : Set α) => ∀ (e : α), e ∈ A → e ∈ B }

instance instHasSSubsetSet {α : Type u_1} : HasSSubset (Set α)

Equations

• instHasSSubsetSet = { SSubset := fun (A B : Set α) => A ⊆ B ∧ ¬B ⊆ A }

instance instSDiffSet {α : Type u_1} : SDiff (Set α)

Equations

• instSDiffSet = { sdiff := fun (A B : Set α) (e : α) => e ∈ A ∧ ¬e ∈ B }

def List.toSet {α : Type u_1} (l : List α) : Set α

Equations

• l.toSet e = (e ∈ l)

def Set.powerset (α : Type u) (S x : Set α) : Prop

Equations

• Set.powerset α S x = (x ⊆ S)

def Set.map {α : Type u_1} {β : Type u_2} (f : α → β) (S : Set α) [Fintype α] : Set β

Equations

• Set.map f S b = ∃ (a : α), a ∈ S ∧ f a = b

theorem Set.ext {α : Type u_1} (X Y : Set α) : (∀ (e : α), e ∈ X ↔ e ∈ Y) → X = Y

theorem Set.inter_commutative {α : Type u_1} (X Y : Set α) : X ∩ Y = Y ∩ X

theorem Set.union_commutative {α : Type u_1} (X Y : Set α) : X ∪ Y = Y ∪ X

theorem Set.distr_inter_union {α : Type u_1} (X Y Z : Set α) : X ∩ (Y ∪ Z) = X ∩ Y ∪ X ∩ Z

theorem Set.distr_union_inter {α : Type u_1} (X Y Z : Set α) : X ∪ Y ∩ Z = (X ∪ Y) ∩ (X ∪ Z)

theorem Set.not_empty_contains_element {α : Type u_1} (X : Set α) : X ≠ ∅ → ∃ (e : α), e ∈ X

theorem Set.empty_eq {α : Type u_1} (A : Set α) : (∀ (x : α), ¬x ∈ A) → A = ∅

theorem Set.empty_iff {α : Type u_1} (A : Set α) : A = ∅ ↔ ∀ (a : α), ¬a ∈ A

theorem Set.ne_empty_contains_element {α : Type u_1} (B : Set α) [DecidableEq (Set α)] : (B != ∅) = true → ∃ (a : α), a ∈ B

theorem Set.empty_set_if_empty_type {α : Type u_1} (T : Fintype α) (S : Set α) : Fintype.elems = [] → S = ∅

theorem Set.complete_set_iff {α : Type u_1} [Fintype α] (S : Set α) : (S = fun (x : α) => True) ↔ ∀ (x : α), x ∈ S

theorem Set.complete_set_eq_fintype_elems {α : Type u_1} (T : Fintype α) : Fintype.elems.toSet = fun (x : α) => True

theorem Set.exists_not_mem_if_ne_complete_set {α : Type u_1} (T : Fintype α) (S : Set α) : (S ≠ fun (x : α) => True) → ∃ (a : α), ¬a ∈ S

theorem Set.ssubset_of_complete_set {α : Type u_1} (T : Fintype α) (S : Set α) : (S ≠ fun (x : α) => True) → S ⊂ fun (x : α) => True

theorem Set.mem_iff {α : Type u_1} {S : Set α} (x : α) : x ∈ S ↔ S x