def Finset' (α : Type u) : Type u

Equations

• Finset' α = List α

instance instMembershipFinset' {α : Type u_1} : Membership α (Finset' α)

Equations

• instMembershipFinset' = { mem := fun (s : Finset' α) (a : α) => List.Mem a s }

def Finset.eq {α : Type u_1} (l k : Finset' α) : Prop

Equations

• Finset.eq l k = ∀ (a : α), a ∈ l ↔ a ∈ k

def Finset.eq.eqv {α : Type u_1} : Equivalence eq

Equations

• ⋯ = ⋯

instance Finset.instSetoid (α : Type u) : Setoid (Finset' α)

Equations

• Finset.instSetoid α = { r := Finset.eq, iseqv := ⋯ }

def Finset (α : Type u) : Type u

Equations

• Finset α = Quotient (Finset.instSetoid α)

def Finset.mk {α : Type u_1} (l : Finset' α) : Finset α

Equations

• Finset.mk l = Quotient.mk (Finset.instSetoid α) l

theorem Finset.perm_if_eq {α : Type u_1} [DecidableEq α] (l k : Finset' α) (eq : eq l k) : (List.removeDups l).Perm (List.removeDups k)

theorem Finset.eq_if_perm {α : Type u_1} [DecidableEq α] (l k : Finset' α) (perm : (List.removeDups l).Perm (List.removeDups k)) : eq l k

theorem Finset.perm_iff_eq {α : Type u_1} [DecidableEq α] (l k : Finset' α) : (List.removeDups l).Perm (List.removeDups k) ↔ eq l k

theorem Finset.length_eq_if_eq {α : Type u_1} [DecidableEq α] (l k : Finset' α) (eq : eq l k) : (List.removeDups l).length = (List.removeDups k).length

def Finset.card {α : Type u_1} [DecidableEq α] : Finset α → Nat

Equations

• Finset.card = Quot.lift (fun (l' : Finset' α) => (List.removeDups l').length) ⋯

def Finset.mem {α : Type u_1} (a : α) : Finset α → Prop

Equations

• Finset.mem a = Quot.lift (fun (s : Finset' α) => a ∈ s) ⋯

def Finset.union {α : Type u_1} : Finset α → Finset α → Finset α

Equations

• Finset.union = Quotient.lift₂ (fun (a b : Finset' α) => Finset.mk (List.append a b)) ⋯

def Finset.insert {α : Type u_1} (a : α) : Finset α → Finset α

Equations

• Finset.insert a = Quot.lift (fun (s : Finset' α) => Finset.mk (a :: s)) ⋯

instance instEmptyCollectionFinset {α : Type u_1} : EmptyCollection (Finset α)

Equations

• instEmptyCollectionFinset = { emptyCollection := Finset.mk [] }

instance instMembershipFinset {α : Type u_1} : Membership α (Finset α)

Equations

• instMembershipFinset = { mem := fun (s : Finset α) (a : α) => Finset.mem a s }

instance instUnionFinset {α : Type u_1} : Union (Finset α)

Equations

• instUnionFinset = { union := fun (X Y : Finset α) => X.union Y }

instance instHasSubsetFinset {α : Type u_1} : HasSubset (Finset α)

Equations

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

theorem mem_list_iff_mem_mk {α : Type u_1} (l' : List α) (a : α) : a ∈ l' ↔ a ∈ Finset.mk l'

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

theorem Finset.ext_iff {α : Type u_1} {X Y : Finset α} : X = Y ↔ ∀ (a : α), a ∈ X ↔ a ∈ Y

instance instDecidableMemFinsetOfDecidableEq {α : Type u_1} [DecidableEq α] (x : α) (S : Finset α) : Decidable (x ∈ S)

Equations

• instDecidableMemFinsetOfDecidableEq x S = Quot.recOnSubsingleton S fun (l : Finset' α) => List.instDecidableMemOfLawfulBEq x l

instance instDecidableMemFinset'OfDecidableEq {α : Type u_1} [DecidableEq α] (l : Finset' α) (a : α) : Decidable (a ∈ l)

Equations

• instDecidableMemFinset'OfDecidableEq l a = List.instDecidableMemOfLawfulBEq a l

def Finset.inter {α : Type u_1} [DecidableEq α] : Finset α → Finset α → Finset α

Equations

• Finset.inter = Quotient.lift₂ (fun (x y : Finset' α) => Finset.mk (List.filter (fun (a : α) => decide (a ∈ y)) x)) ⋯

instance instInterFinsetOfDecidableEq {α : Type u_1} [DecidableEq α] : Inter (Finset α)

Equations

• instInterFinsetOfDecidableEq = { inter := fun (A B : Finset α) => A.inter B }

theorem Finset.eq_rfl {α : Type u_1} (X : Finset α) : X = X

instance Finset.eq.decidable {α : Type u_1} [DecidableEq α] (l k : Finset' α) : Decidable (eq l k)

Equations

• Finset.eq.decidable l k = if sub1 : List.Subset l k then if sub2 : List.Subset k l then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance instDecidableEquivFinset'OfDecidableEq {α : Type u_1} [DecidableEq α] (l k : Finset' α) : Decidable (l ≈ k)

Equations

• instDecidableEquivFinset'OfDecidableEq l k = Finset.eq.decidable l k

instance instDecidableEqFinset {α : Type u_1} [DecidableEq α] : DecidableEq (Finset α)

Equations

• instDecidableEqFinset x✝¹ x✝ = Quotient.recOnSubsingleton₂ x✝¹ x✝ fun (repr_a repr_b : Finset' α) => if eq : repr_a ≈ repr_b then isTrue ⋯ else isFalse ⋯

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

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

def Finset.toSet {α : Type u_1} (S : Finset α) : Set α

Equations

• S.toSet x = (x ∈ S)

theorem Finset.mem_toSet {α : Type u_1} (S : Finset α) (x : α) : x ∈ S ↔ x ∈ S.toSet

theorem Finset.inter_eq {α : Type u_1} [DecidableEq α] (l k : Finset' α) : mk l ∩ mk k = mk (List.filter (fun (x : α) => decide (x ∈ k)) l)

theorem Finset.mem_inter {α : Type u_1} [DecidableEq α] (X Y : Finset α) (a : α) : a ∈ X ∩ Y ↔ a ∈ X ∧ a ∈ Y