Foundation.Vorspiel.AdjunctiveSet

source

class Adjoin (β : outParam (Type u_1)) (α : Type u_2) :

Type (max u_1 u_2)

adjoin : β → α → α

Instances

source

@[implicit_reducible]

instance instAdjoinSet (α : Type u_1) :

Adjoin α (Set α)

Equations

instAdjoinSet α = { adjoin := insert }

source

@[implicit_reducible]

instance instAdjoinList (α : Type u_1) :

Adjoin α (List α)

Equations

instAdjoinList α = { adjoin := List.cons }

source

@[implicit_reducible]

instance instAdjoinMultiset (α : Type u_1) :

Adjoin α (Multiset α)

Equations

instAdjoinMultiset α = { adjoin := Multiset.cons }

source

@[implicit_reducible]

instance instAdjoinFinsetOfDecidableEq (α : Type u_1) [DecidableEq α] :

Adjoin α (Finset α)

Equations

instAdjoinFinsetOfDecidableEq α = { adjoin := insert }

source

class AdjunctiveSet (β : outParam (Type u_1)) (α : Type u_2) extends Membership β α, HasSubset α, EmptyCollection α, Adjoin β α :

Type (max u_1 u_2)

mem : α → β → Prop
Subset : α → α → Prop
emptyCollection : α
adjoin : β → α → α
subset_iff {a b : α} : a ⊆ b ↔ ∀ x ∈ a, x ∈ b
not_mem_empty (x : β) : x ∉ ∅
mem_cons_iff {x z : β} {a : α} : x ∈ adjoin z a ↔ x = z ∨ x ∈ a

Instances

source

@[implicit_reducible]

instance Set.adjunctiveSet {α : Type u_1} :

AdjunctiveSet α (Set α)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance List.adjunctiveSet {α : Type u_1} :

AdjunctiveSet α (List α)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance Multiset.adjunctiveSet {α : Type u_1} :

AdjunctiveSet α (Multiset α)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance Finset.adjunctiveSet {α : Type u_1} [DecidableEq α] :

AdjunctiveSet α (Finset α)

Equations

One or more equations did not get rendered due to their size.

source

def AdjunctiveSet.set {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] :

α → Set β

Equations

AdjunctiveSet.set a = {x : β | x ∈ a}

Instances For

source

@[simp]

theorem AdjunctiveSet.mem_set_iff {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {x : β} {a : α} :

x ∈ set a ↔ x ∈ a

source

theorem AdjunctiveSet.subset_iff_set_subset_set {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b : α} :

a ⊆ b ↔ set a ⊆ set b

source

@[simp]

theorem AdjunctiveSet.subset_refl {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) :

a ⊆ a

source

theorem AdjunctiveSet.subset_trans {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b c : α} (ha : a ⊆ b) (hb : b ⊆ c) :

a ⊆ c

source

theorem AdjunctiveSet.subset_antisymm {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b : α} (ha : a ⊆ b) (hb : b ⊆ a) :

set a = set b

source

@[simp]

theorem AdjunctiveSet.empty_subset {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) :

∅ ⊆ a

source

@[simp]

theorem AdjunctiveSet.mem_cons {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) (x : β) :

x ∈ adjoin x a

source

@[simp]

theorem AdjunctiveSet.subset_cons {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) (x : β) :

a ⊆ adjoin x a

source

@[simp]

theorem AdjunctiveSet.set_empty {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] :

set ∅ = ∅

source

@[simp]

theorem AdjunctiveSet.set_cons {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (z : β) (a : α) :

set (adjoin z a) = insert z (set a)

source

def AdjunctiveSet.Finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) :

Prop

Equations

AdjunctiveSet.Finite a = (AdjunctiveSet.set a).Finite

Instances For

source

@[simp]

theorem AdjunctiveSet.empty_finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] :

Finite ∅

source

theorem AdjunctiveSet.Finite.of_subset {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b : α} (ha : Finite a) (h : b ⊆ a) :

Finite b

source

@[simp]

theorem AdjunctiveSet.cons_finite_iff {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {z : β} {a : α} :

Finite (adjoin z a) ↔ Finite a

source

def AdjunctiveSet.addList {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) :

List β → α

Equations

AdjunctiveSet.addList a [] = a
AdjunctiveSet.addList a (x_1 :: xs) = adjoin x_1 (AdjunctiveSet.addList a xs)

Instances For

source

def List.toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] :

List β → α

Equations

[].toAdjunctiveSet = ∅
(x_1 :: xs).toAdjunctiveSet = adjoin x_1 xs.toAdjunctiveSet

Instances For

source

noncomputable def Finset.toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] :

Finset β → α

Equations

s.toAdjunctiveSet = s.toList.toAdjunctiveSet

Instances For

source

@[simp]

theorem AdjunctiveSet.mem_list_toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {x : β} {l : List β} :

x ∈ l.toAdjunctiveSet ↔ x ∈ l

source

@[simp]

theorem AdjunctiveSet.mem_finset_toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {x : β} {s : Finset β} :

x ∈ s.toAdjunctiveSet ↔ x ∈ s

source

@[simp]

theorem AdjunctiveSet.list_toAdjunctiveSet_finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (l : List β) :

Finite l.toAdjunctiveSet

source

@[simp]

theorem AdjunctiveSet.finset_toAdjunctiveSet_finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (s : Finset β) :

Finite s.toAdjunctiveSet

source

theorem Set.cons_eq {α : Type u_1} (a : α) (s : Set α) :

adjoin a s = insert a s

source

@[simp]

theorem Set.adjunctiveSet_set {α : Type u_1} (s : Set α) :

AdjunctiveSet.set s = s

source

@[simp]

theorem Set.adjunctiveSet_finite_iff {α : Type u_1} (s : Set α) :

AdjunctiveSet.Finite s ↔ s.Finite