Projects.Util.Data.Set

source

structure Set' (α : Type u) [hh₁ : DecidableEq α] [hh₂ : Hashable α] :

Type u

inner : Std.ExtDHashMap α fun (x : α) => Unit

Instances For

source

@[instance_reducible]

instance instInhabitedSet' {a✝ : Type u_1} {a✝¹ : DecidableEq a✝} {a✝² : Hashable a✝} :

Inhabited (Set' a✝)

Equations

instInhabitedSet' = { default := instInhabitedSet'.default }

source

def Set'.empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Set' α

Equations

Set'.empty = { inner := ∅ }

Instances For

source

@[instance_reducible]

instance Set'.instEmptyCollection {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

EmptyCollection (Set' α)

Equations

Set'.instEmptyCollection = { emptyCollection := Set'.empty }

source

theorem Set'.empty_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅ = { inner := ∅ }

source

def Set'.insertP {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (x : α) (s : Set' α) :

Set' α

Equations

Set'.insertP x s = { inner := insert ⟨x, ()⟩ s.inner }

Instances For

source

@[instance_reducible]

instance Set'.instInsert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Insert α (Set' α)

Equations

Set'.instInsert = { insert := Set'.insertP }

source

theorem Set'.insert_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} {s : Set' α} :

insert x s = { inner := insert ⟨x, ()⟩ s.inner }

source

def Set'.insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (i : α) :

Set' α

Equations

s.insert i = { inner := s.inner.insert i () }

Instances For

source

def Set'.ofList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (xs : List α) :

Set' α

Equations

Set'.ofList xs = { inner := Std.ExtDHashMap.ofList (List.map (fun (x : α) => ⟨x, ()⟩) xs) }

Instances For

source

def Set'.mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (i : α) :

Prop

Equations

s.mem i = (i ∈ s.inner)

Instances For

source

@[instance_reducible]

instance Set'.instMembership {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Membership α (Set' α)

Equations

Set'.instMembership = { mem := Set'.mem }

source

theorem Set'.mem_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {i : α} :

i ∈ s ↔ i ∈ s.inner

source

@[instance_reducible]

instance Set'.instDecidableMem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {i : α} :

Decidable (s.mem i)

Equations

Set'.instDecidableMem = id inferInstance

source

@[instance_reducible]

instance Set'.instDecidableMem_1 {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {i : α} :

Decidable (i ∈ s)

Equations

Set'.instDecidableMem_1 = id inferInstance

source

def Set'.toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] (s : Set' α) :

List α

Equations

s.toList = Std.ExtDHashMap.lift (fun (x : Std.DHashMap α fun (x : α) => Unit) => x.toSortedKeys) ⋯ s.inner

Instances For

source

@[simp]

theorem Set'.ofList_nil {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

ofList [] = ∅

source

@[simp]

theorem Set'.ofList_snoc {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List α} {x : α} :

ofList (xs ++ [x]) = insertP x (ofList xs)

source

@[simp]

theorem Set'.toList_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [LinearOrder α] :

∅.toList = []

source

@[simp]

theorem Set'.mem_insertP {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x i : α} :

i ∈ insertP x s ↔ i = x ∨ i ∈ s

source

@[simp]

theorem Set'.mem_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {i j : α} :

j ∈ s.insert i ↔ j = i ∨ j ∈ s

source

@[simp]

theorem Set'.mem_insert' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x i : α} :

i ∈ insert x s ↔ i = x ∨ i ∈ s

source

@[simp]

theorem Set'.mem_ofList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List α} {i : α} :

i ∈ ofList xs ↔ i ∈ xs

source

theorem Set'.eq_empty_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s = ∅ ↔ ∀ (i : α), i ∉ s

source

@[simp]

theorem Set'.not_mem_empty' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {i : α} :

¬∅.mem i

source

@[simp]

theorem Set'.not_mem_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {i : α} :

i ∉ ∅

source

theorem Set'.ext_iff' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ = s₂ ↔ s₁.inner.inner.out.Equiv s₂.inner.inner.out

source

theorem Set'.ext' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁.inner.inner.out.Equiv s₂.inner.inner.out) :

s₁ = s₂

source

theorem Set'.ext_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ = s₂ ↔ ∀ (i : α), i ∈ s₁ ↔ i ∈ s₂

source

theorem Set'.ext {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : ∀ (i : α), i ∈ s₁ ↔ i ∈ s₂) :

s₁ = s₂

source

theorem Set'.ofList_eq_ofList_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs ys : List α} (hx : xs.Nodup) (hy : ys.Nodup) :

ofList xs = ofList ys ↔ xs.Perm ys

source

def Set'.univ {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : Fintype α] :

Set' α

Equations

Set'.univ = { inner := Std.ExtDHashMap.range fun (x : α) => () }

Instances For

source

@[simp]

theorem Set'.mem_univ {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : Fintype α] {i : α} :

i ∈ univ

source

@[simp]

theorem Set'.nonempty_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

insert x s ≠ ∅

source

@[simp]

theorem Set'.nodup_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [LinearOrder α] :

s.toList.Nodup

source

@[simp]

theorem Set'.sortedLE_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [LinearOrder α] :

s.toList.SortedLE

source

@[simp]

theorem Set'.mem_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [LinearOrder α] {x : α} :

x ∈ s.toList ↔ x ∈ s

source

@[simp]

theorem Set'.toList_eq_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [LinearOrder α] {s₁ s₂ : Set' α} :

s₁.toList = s₂.toList ↔ s₁ = s₂

source

@[simp]

theorem Set'.toList_eq_nil_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [LinearOrder α] :

s.toList = [] ↔ s = ∅

source

def Set'.toDMap {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) :

DMap α fun (x : α) => Unit

Equations

s.toDMap = { inner := s.inner }

Instances For

source

@[instance_reducible]

instance Set'.instDecidableEq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

DecidableEq (Set' α)

Equations

s₁.instDecidableEq s₂ = match h : decide (s₁.inner = s₂.inner) with | true => isTrue ⋯ | false => isFalse ⋯

source

@[instance_reducible]

instance Set'.instInhabitedSet {α : Type u} :

Inhabited (Set α)

Equations

Set'.instInhabitedSet = { default := ∅ }

source

def Set'.values {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] (s : Set' α) :

List α

Equations

s.values = s.inner.keys

Instances For

source

@[simp]

theorem Set'.mem_values {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [LinearOrder α] {i : α} :

i ∈ s.values ↔ i ∈ s

source

def Set'.all {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (p : α → Bool) :

Bool

Equations

s.all p = s.inner.all fun (i : α) (x : Unit) => p i

Instances For

source

theorem Set'.forall_mem_iff_all {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Prop} [hp : DecidablePred p] :

(∀ x ∈ s, p x) ↔ (s.all fun (b : α) => decide (p b)) = true

source

@[instance_reducible]

instance Set'.instDecidableForallForallMemOfDecidablePred {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Prop} [hp : DecidablePred p] :

Decidable (∀ x ∈ s, p x)

Equations

Set'.instDecidableForallForallMemOfDecidablePred = match h : s.all fun (b : α) => decide (p b) with | true => isTrue ⋯ | false => isFalse ⋯

source

@[simp]

theorem Set'.all_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Prop} [DecidablePred p] :

(s.all fun (b : α) => decide (p b)) = decide (∀ x ∈ s, p x)

source

@[instance_reducible]

instance Set'.instFintype {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : Fintype α] :

Fintype (Set' α)

Equations

Set'.instFintype = { elems := Finset.map { toFun := Set'.mk, inj' := ⋯ } Fintype.elems, complete := ⋯ }

source

instance Set'.instFinite {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : Finite α] :

Finite (Set' α)

source

def Set'.fold {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (f : β → α → β) (z : β) (h_assoc : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x) :

Equations

s.fold f z h_assoc = s.inner.fold (fun (acc : β) (x : α) (x_1 : Unit) => f acc x) z ⋯

Instances For

source

def Set'.fold₁ {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (f : α → α → α) (h_comm : ∀ {x y : α}, f x y = f y x) (h_assoc : ∀ {acc x y : α}, f (f acc x) y = f (f acc y) x) :

Option α

Equations

s.fold₁ f h_comm h_assoc = s.fold (fun (acc : Option α) (x : α) => some (acc.elim x fun (x_1 : α) => f x_1 x)) none ⋯

Instances For

source

theorem Set'.fold_eq_foldl_toList {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {z : β} {f : β → α → β} {h_assoc : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x} :

s.fold f z h_assoc = List.foldl f z s.toList

source

theorem Set'.eq_iff_inner_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ = s₂ ↔ s₁.inner = s₂.inner

source

theorem Set'.eq_iff_toList_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {s₁ s₂ : Set' α} :

s₁ = s₂ ↔ s₁.toList = s₂.toList

source

@[simp]

theorem Set'.ofList_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

ofList s.toList = s

source

theorem Set'.toList_ofList_perm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {xs : List α} (h : xs.Nodup) :

(ofList xs).toList.Perm xs

source

theorem Set'.ind_ofList' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {p : Set' α → Prop} (h : ∀ (xs : List α), xs.Nodup → xs.SortedLE → p (ofList xs)) (s : Set' α) :

p s

source

def Set'.min? {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] (s : Set' α) :

Option α

Equations

s.min? = s.inner.minKey?

Instances For

source

def Set'.max? {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] (s : Set' α) :

Option α

Equations

s.max? = s.inner.maxKey?

Instances For

source

def Set'.min! {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (s : Set' α) :

Equations

s.min! = s.min?.get!

Instances For

source

def Set'.max! {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (s : Set' α) :

Equations

s.max! = s.max?.get!

Instances For

source

theorem Set'.min?_eq_head?_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

s.min? = s.toList.head?

source

theorem Set'.maxKey?_eq_getLast?_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

s.max? = s.toList.getLast?

source

@[simp]

theorem Set'.min?_eq_none_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

s.min? = none ↔ s = ∅

source

@[simp]

theorem Set'.max?_eq_none_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

s.max? = none ↔ s = ∅

source

theorem Set'.not_mem_of_lt_min? {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {m x : α} (h₁ : s.min? = some m) (h₂ : x < m) :

x ∉ s

source

theorem Set'.not_mem_of_max?_lt {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {m x : α} (h₁ : s.max? = some m) (h₂ : m < x) :

x ∉ s

source

theorem Set'.not_mem_of_lt_min! {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₁✝ : Inhabited α] [ha₂✝ : LinearOrder α] {x : α} (h : x < s.min!) :

x ∉ s

source

theorem Set'.not_mem_of_max!_lt {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₁✝ : Inhabited α] [ha₂✝ : LinearOrder α] {x : α} (h : s.max! < x) :

x ∉ s

source

theorem Set'.min?_le_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {m x : α} (h₁ : s.min? = some m) (h₂ : x ∈ s) :

m ≤ x

source

theorem Set'.le_max?_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {m x : α} (h₁ : s.max? = some m) (h₂ : x ∈ s) :

x ≤ m

source

theorem Set'.min!_le_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₁✝ : Inhabited α] [ha₂✝ : LinearOrder α] {x : α} (h : x ∈ s) :

s.min! ≤ x

source

theorem Set'.le_max!_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₁✝ : Inhabited α] [ha₂✝ : LinearOrder α] {x : α} (h : x ∈ s) :

x ≤ s.max!

source

def Set'.subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s s' : Set' α) :

Prop

Equations

s.subset s' = ∀ x ∈ s, x ∈ s'

Instances For

source

@[instance_reducible]

instance Set'.instHasSubset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

HasSubset (Set' α)

Equations

Set'.instHasSubset = { Subset := Set'.subset }

source

theorem Set'.subset_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s s' : Set' α} :

s ⊆ s' ↔ ∀ x ∈ s, x ∈ s'

source

def Set'.subset_comp {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s s' : Set' α) :

Bool

Equations

s.subset_comp s' = s.all fun (x : α) => decide (x ∈ s')

Instances For

source

theorem Set'.subset_iff_subset_comp {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s s' : Set' α} :

s ⊆ s' ↔ s.subset_comp s' = true

source

@[instance_reducible]

instance Set'.instDecidableSubset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s s' : Set' α} :

Decidable (s ⊆ s')

Equations

Set'.instDecidableSubset = match h : s.subset_comp s' with | true => isTrue ⋯ | false => isFalse ⋯

source

@[simp]

theorem Set'.subset_comp_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s s' : Set' α} :

s.subset_comp s' = decide (s ⊆ s')

source

@[simp]

theorem Set'.subset_refl {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s ⊆ s

source

theorem Set'.subset_trans {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} (h₁ : s₁ ⊆ s₂) (h₂ : s₂ ⊆ s₃) :

s₁ ⊆ s₃

source

theorem Set'.insert_comm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x y : α} :

(s.insert x).insert y = (s.insert y).insert x

source

theorem Set'.ind {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {p : Set' α → Prop} (h₁ : p ∅) (h₂ : ∀ (s : Set' α), ∀ x ∉ s, p s → p (s.insert x)) (s : Set' α) :

p s

source

def Set'.union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s₁ s₂ : Set' α) :

Set' α

Equations

s₁.union s₂ = s₂.fold (fun (s : Set' α) (x : α) => s.insert x) s₁ ⋯

Instances For

source

@[instance_reducible]

instance Set'.instUnion {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Union (Set' α)

Equations

Set'.instUnion = { union := Set'.union }

source

theorem Set'.union_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∪ s₂ = s₁.union s₂

source

@[simp]

theorem Set'.fold_empty {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {f : β → α → β} {z : β} {h : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x} :

∅.fold f z h = z

source

theorem Set'.fold_insert' {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {f : β → α → β} {z : β} {h : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x} {x : α} (h₁ : x ∉ s) :

(s.insert x).fold f z h = s.fold f (f z x) ⋯

source

@[simp]

theorem Set'.mem_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

x ∈ s₁ ∪ s₂ ↔ x ∈ s₁ ∨ x ∈ s₂

source

def Set'.ofFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Finset α) :

Set' α

Equations

Set'.ofFinset s = Quotient.liftWith s.val Set'.ofList ⋯

Instances For

source

@[simp]

theorem Set'.mem_ofFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Finset α} {x : α} :

x ∈ ofFinset s ↔ x ∈ s

source

noncomputable def Set'.ofSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set α) :

Set' α

Equations

Set'.ofSet s = if h : s.Finite then Set'.ofFinset s.toFinset else ∅

Instances For

source

theorem Set'.mem_ofSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set α} {x : α} (h : s.Finite) :

x ∈ ofSet s ↔ x ∈ s

source

@[instance_reducible]

instance Set'.instCoeList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Coe (List α) (Set' α)

Equations

Set'.instCoeList = { coe := Set'.ofList }

source

@[instance_reducible]

instance Set'.instCoeFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Coe (Finset α) (Set' α)

Equations

Set'.instCoeFinset = { coe := Set'.ofFinset }

source

@[instance_reducible]

noncomputable instance Set'.instCoeSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Coe (Set α) (Set' α)

Equations

Set'.instCoeSet = { coe := Set'.ofSet }

source

def Set'.filter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (p : α → Bool) :

Set' α

Equations

s.filter p = { inner := Std.ExtDHashMap.filter (fun (x : α) (x_1 : Unit) => p x) s.inner }

Instances For

source

@[simp]

theorem Set'.mem_filter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} {x : α} :

x ∈ s.filter p ↔ x ∈ s ∧ p x = true

source

def Set'.diff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s₁ s₂ : Set' α) :

Set' α

Equations

s₁.diff s₂ = s₁.filter fun (x : α) => decide (x ∉ s₂)

Instances For

source

@[instance_reducible]

instance Set'.instSDiff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

SDiff (Set' α)

Equations

Set'.instSDiff = { sdiff := Set'.diff }

source

theorem Set'.diff_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ \ s₂ = s₁.diff s₂

source

@[simp]

theorem Set'.mem_diff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

x ∈ s₁ \ s₂ ↔ x ∈ s₁ ∧ x ∉ s₂

source

def Set'.inter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s₁ s₂ : Set' α) :

Set' α

Equations

s₁.inter s₂ = s₁.filter fun (x : α) => decide (x ∈ s₂)

Instances For

source

@[instance_reducible]

instance Set'.instInter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

Inter (Set' α)

Equations

Set'.instInter = { inter := Set'.inter }

source

theorem Set'.inter_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∩ s₂ = s₁.inter s₂

source

@[simp]

theorem Set'.mem_inter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

x ∈ s₁ ∩ s₂ ↔ x ∈ s₁ ∧ x ∈ s₂

source

@[simp]

theorem Set'.inter_left_subset_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∩ s₂ ⊆ s₁

source

@[simp]

theorem Set'.inter_right_subset_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₂ ∩ s₁ ⊆ s₁

source

theorem Set'.inter_subset_inter_of_left {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} (h : s₁ ⊆ s₂) :

s₁ ∩ s₃ ⊆ s₂ ∩ s₃

source

theorem Set'.inter_subset_inter_of_right {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} (h : s₁ ⊆ s₂) :

s₃ ∩ s₁ ⊆ s₃ ∩ s₂

source

theorem Set'.insert_eq_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∈ s) :

s.insert x = s

source

@[simp]

theorem Set'.insert_idemp {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

(s.insert x).insert x = s.insert x

source

def Set'.map {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] (s : Set' α) (f : α → β) :

Set' β

Equations

s.map f = s.fold (fun (s' : Set' β) (x : α) => s'.insert (f x)) ∅ ⋯

Instances For

source

@[simp]

theorem Set'.map_empty {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {f : α → β} :

∅.map f = ∅

source

@[simp]

theorem Set'.map_insert {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → β} {x : α} :

(s.insert x).map f = (s.map f).insert (f x)

source

@[simp]

theorem Set'.mem_map {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → β} {y : β} :

y ∈ s.map f ↔ ∃ x ∈ s, f x = y

source

theorem Set'.eq_empty_iff_not_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s = ∅ ↔ ∀ (x : α), x ∉ s

source

@[simp]

theorem Set'.map_eq_empty_iff {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → β} :

s.map f = ∅ ↔ s = ∅

source

@[simp]

theorem Set'.empty_eq_map_iff {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → β} :

∅ = s.map f ↔ s = ∅

source

@[simp]

theorem Set'.map_map {α : Type u} {β : Type v} {γ : Type w} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] [hc₁ : DecidableEq γ] [hc₂ : Hashable γ] {s : Set' α} {f : α → β} {g : β → γ} :

(s.map f).map g = s.map fun (x : α) => g (f x)

source

@[simp]

theorem Set'.map_id {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.map id = s

source

@[simp]

theorem Set'.map_id' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

(s.map fun (x : α) => x) = s

source

def Set'.erase {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (x : α) :

Set' α

Equations

s.erase x = { inner := s.inner.erase x }

Instances For

source

@[simp]

theorem Set'.mem_erase {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x y : α} :

y ∈ s.erase x ↔ x ≠ y ∧ y ∈ s

source

theorem Set'.erase_eq_of_not_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∉ s) :

s.erase x = s

source

def Set'.toSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) :

Set α

Equations

s.toSet = {x : α | x ∈ s}

Instances For

source

@[simp]

theorem Set'.mem_toSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

x ∈ s.toSet ↔ x ∈ s

source

@[simp]

theorem Set'.toSet_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.toSet = ∅

source

@[simp]

theorem Set'.toSet_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

(s.insert x).toSet = insert x s.toSet

source

theorem Set'.toSet_ofSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set α} (h : s.Finite) :

(ofSet s).toSet = s

source

def Set'.size {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) :

ℕ

Equations

s.size = s.inner.size

Instances For

source

def Set'.count {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (p : α → Bool) :

ℕ

Equations

s.count p = s.inner.count fun (x : α) (x_1 : Unit) => p x

Instances For

source

@[simp]

theorem Set'.size_filter_eq_count {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} :

(s.filter p).size = s.count p

source

theorem Set'.count_eq_size_filter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} :

s.count p = (s.filter p).size

source

@[simp]

theorem Set'.count_le_size {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} :

s.count p ≤ s.size

source

@[simp]

theorem Set'.count_eq_zero_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} :

s.count p = 0 ↔ ∀ x ∈ s, ¬p x = true

source

@[simp]

theorem Set'.count_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {p : α → Bool} :

∅.count p = 0

source

theorem Set'.count_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} {i : α} (h : i ∉ s) :

(s.insert i).count p = s.count p + if p i = true then 1 else 0

source

theorem Set'.subset_iff_exi_disj_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ⊆ s₂ ↔ ∃ (s₃ : Set' α), (∀ x ∈ s₃, x ∉ s₁) ∧ s₁ ∪ s₃ = s₂

source

theorem Set'.subset_iff_exi_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ⊆ s₂ ↔ ∃ (s₃ : Set' α), s₁ ∪ s₃ = s₂

source

@[simp]

theorem Set'.size_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.size = 0

source

@[simp]

theorem Set'.empty_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

∅ ∪ s = s

source

@[simp]

theorem Set'.union_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s ∪ ∅ = s

source

@[simp]

theorem Set'.empty_inter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

∅ ∩ s = ∅

source

@[simp]

theorem Set'.inter_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s ∩ ∅ = ∅

source

@[simp]

theorem Set'.empty_diff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

∅ \ s = ∅

source

@[simp]

theorem Set'.diff_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s \ ∅ = s

source

@[simp]

theorem Set'.size_eq_zero_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.size = 0 ↔ s = ∅

source

theorem Set'.size_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∉ s) :

(s.insert x).size = s.size + 1

source

theorem Set'.erase_eq_empty_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

s.erase x = ∅ ↔ ∀ y ∈ s, y = x

source

theorem Set'.mem_iff_of_size_eq_one {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x y : α} (h₁ : s.size = 1) (h₂ : x ∈ s) :

y ∈ s ↔ y = x

source

theorem Set'.eq_of_size_eq_one_and_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x y : α} (h₁ : s.size = 1) (h₂ : x ∈ s) (h₃ : y ∈ s) :

x = y

source

theorem Set'.size_eq_one_of_size_le_one_and_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h₁ : s.size ≤ 1) (h₂ : x ∈ s) :

s.size = 1

source

theorem Set'.insert_erase_eq_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∈ s) :

(s.erase x).insert x = s

source

theorem Set'.eq_insert_erase_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∈ s) :

s = (s.erase x).insert x

source

theorem Set'.size_erase_add_one {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∈ s) :

(s.erase x).size + 1 = s.size

source

theorem Set'.size_erase {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∈ s) :

(s.erase x).size = s.size - 1

source

theorem Set'.diff_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

s₁ \ s₂.insert x = (s₁ \ s₂).erase x

source

theorem Set'.erase_diff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

(s₁ \ s₂).erase x = s₁ \ s₂.insert x

source

@[simp]

theorem Set'.union_eq_empty_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∪ s₂ = ∅ ↔ s₁ = ∅ ∧ s₂ = ∅

source

@[simp]

theorem Set'.erase_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

∅.erase x = ∅

source

theorem Set'.diff_eq_empty_iff_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ \ s₂ = ∅ ↔ s₁ ⊆ s₂

source

theorem Set'.subset_antisymm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h₁ : s₁ ⊆ s₂) (h₂ : s₂ ⊆ s₁) :

s₁ = s₂

source

@[simp]

theorem Set'.union_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s ∪ s = s

source

@[simp]

theorem Set'.inter_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s ∩ s = s

source

@[simp]

theorem Set'.diff_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s \ s = ∅

source

theorem Set'.exi_mem_of_ne_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} (h : s ≠ ∅) :

∃ (x : α), x ∈ s

source

theorem Set'.ne_empty_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : x ∈ s) :

s ≠ ∅

source

theorem Set'.eq_empty_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h₁ : s₁ ⊆ s₂) (h₂ : s₂ = ∅) :

s₁ = ∅

source

theorem Set'.ne_empty_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h₁ : s₁ ⊆ s₂) (h₂ : s₁ ≠ ∅) :

s₂ ≠ ∅

source

@[simp]

theorem Set'.insert_ne_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

s.insert x ≠ ∅

source

theorem Set'.disjoint_comm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(∀ x ∈ s₁, x ∉ s₂) ↔ ∀ x ∈ s₂, x ∉ s₁

source

theorem Set'.diff_eq_left_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ \ s₂ = s₁ ↔ ∀ x ∈ s₁, x ∉ s₂

source

theorem Set'.diff_eq_left_iff' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ \ s₂ = s₁ ↔ ∀ x ∈ s₂, x ∉ s₁

source

@[simp]

theorem Set'.diff_eq_right_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ \ s₂ = s₂ ↔ s₁ = ∅ ∧ s₂ = ∅

source

theorem Set'.mem_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} (h : s₁ ⊆ s₂) (hx : x ∈ s₁) :

x ∈ s₂

source

theorem Set'.not_mem_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} (h : s₁ ⊆ s₂) (hx : x ∉ s₂) :

x ∉ s₁

source

theorem Set'.ne_empty_of_size_ne_zero {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} (h : s.size ≠ 0) :

s ≠ ∅

source

theorem Set'.ne_empty_of_size_eq_add_one {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {n : ℕ} (h : s.size = n + 1) :

s ≠ ∅

source

theorem Set'.size_eq_one_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.size = 1 ↔ ∃ x ∈ s, ∀ y ∈ s, y = x

source

theorem Set'.size_eq_one_of {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (hx : x ∈ s) (h : ∀ y ∈ s, y = x) :

s.size = 1

source

theorem Set'.eq_insert_empty_of_size_eq_one {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (h : s.size = 1) (hx : x ∈ s) :

s = ∅.insert x

source

@[simp]

theorem Set'.erase_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

s.erase x ⊆ s

source

@[simp]

theorem Set'.empty_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

∅ ⊆ s

source

def Set'.toMap {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) (f : α → β) :

Map α β

Equations

s.toMap f = { inner := Std.ExtDHashMap.map (fun (x : α) (x_1 : Unit) => f x) s.inner }

Instances For

source

@[simp]

theorem Set'.mem_toMap {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {f : α → β} {i : α} :

i ∈ s.toMap f ↔ i ∈ s

source

@[simp]

theorem Set'.get?_toMap_eq_some_iff {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {f : α → β} {i : α} {x : β} :

Map.get? i (s.toMap f) = some x ↔ i ∈ s ∧ f i = x

source

@[simp]

theorem Set'.toMap_empty {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {f : α → β} :

∅.toMap f = ∅

source

@[simp]

theorem Set'.mem_list_foldl_map_push_iff {α : Type u} {β : Type v} [hb₁ : DecidableEq β] [hb₂ : Hashable β] {xs : List α} {f : α → β} {y : β} {mp : Map β ℕ} :

y ∈ List.foldl (fun (mp : Map β ℕ) (x : α) => mp.push (f x)) mp xs ↔ y ∈ mp ∨ ∃ x ∈ xs, f x = y

source

theorem Set'.toList_erase {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {x : α} :

(s.erase x).toList = s.toList.erase x

source

theorem Set'.count_eq_countP_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] {p : α → Bool} :

s.count p = List.countP p s.toList

source

theorem Set'.fold_map_push_eq_map_toMap {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → β} :

s.fold (fun (mp : Map β ℕ) (x : α) => mp.push (f x)) ∅ ⋯ = (s.map f).toMap fun (x : β) => s.count fun (x_1 : α) => decide (f x_1 = x)

source

theorem Set'.fold_map_push_eq_toMap {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.fold (fun (mp : Map α ℕ) (x : α) => mp.push x) ∅ ⋯ = s.toMap fun (x : α) => s.count fun (y : α) => decide (y = x)

source

theorem Set'.get?_toMap_eq {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {f : α → β} {x : α} :

Map.get? x (s.toMap f) = if x ∈ s then some (f x) else none

source

@[simp]

theorem Set'.length_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

s.toList.length = s.size

source

@[simp]

theorem Set'.size_toMap {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {f : α → β} :

(s.toMap f).size = s.size

source

theorem Set'.size_ofList_of_nodup {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List α} (h : xs.Nodup) :

(ofList xs).size = xs.length

source

@[simp]

theorem Set'.size_ofFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Finset α} :

(ofFinset s).size = s.card

source

@[simp]

theorem Set'.subset_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

s ⊆ s.insert x

source

def Set'.unionList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (xs : List (Set' α)) :

Set' α

Equations

Set'.unionList xs = List.foldl (fun (x1 x2 : Set' α) => x1 ∪ x2) ∅ xs

Instances For

source

@[simp]

theorem Set'.unionList_nil {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

unionList [] = ∅

source

theorem Set'.union_comm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∪ s₂ = s₂ ∪ s₁

source

theorem Set'.inter_comm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∩ s₂ = s₂ ∩ s₁

source

theorem Set'.union_assoc {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} :

s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)

source

theorem Set'.inter_assoc {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} :

s₁ ∩ s₂ ∩ s₃ = s₁ ∩ (s₂ ∩ s₃)

source

@[simp]

theorem Set'.unionList_cons {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {xs : List (Set' α)} :

unionList (s :: xs) = s ∪ unionList xs

source

@[simp]

theorem Set'.unionList_append {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs ys : List (Set' α)} :

unionList (xs ++ ys) = unionList xs ∪ unionList ys

source

theorem Set'.unionList_of_perm {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs ys : List (Set' α)} (h : xs.Perm ys) :

unionList xs = unionList ys

source

@[simp]

theorem Set'.mem_unionList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List (Set' α)} {x : α} :

x ∈ unionList xs ↔ ∃ s ∈ xs, x ∈ s

source

theorem Set'.size_le_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ⊆ s₂) :

s₁.size ≤ s₂.size

source

theorem Set'.size_eq_size_add_one_of {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : ∃ x ∉ s₂, s₁ = s₂.insert x) :

s₁.size = s₂.size + 1

source

theorem Set'.size_inter_insert_left {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} (h₁ : x ∉ s₁) (h₂ : x ∈ s₂) :

(s₁.insert x ∩ s₂).size = (s₁ ∩ s₂).size + 1

source

theorem Set'.size_inter_insert_right {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} (h₁ : x ∈ s₁) (h₂ : x ∉ s₂) :

(s₁ ∩ s₂.insert x).size = (s₁ ∩ s₂).size + 1

source

theorem Set'.insert_inter_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} (h : x ∈ s₂) :

s₁.insert x ∩ s₂ = (s₁ ∩ s₂).insert x

source

theorem Set'.inter_insert_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} (h : x ∈ s₁) :

s₁ ∩ s₂.insert x = (s₁ ∩ s₂).insert x

source

theorem Set'.subset_of_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ = s₂) :

s₁ ⊆ s₂

source

theorem Set'.subset_of_inter_eq_left {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ∩ s₂ = s₁) :

s₁ ⊆ s₂

source

theorem Set'.subset_of_inter_eq_right {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ∩ s₂ = s₂) :

s₂ ⊆ s₁

source

theorem Set'.inter_eq_left_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ⊆ s₂) :

s₁ ∩ s₂ = s₁

source

theorem Set'.inter_eq_right_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₂ ⊆ s₁) :

s₁ ∩ s₂ = s₂

source

@[simp]

theorem Set'.inter_eq_left_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∩ s₂ = s₁ ↔ s₁ ⊆ s₂

source

@[simp]

theorem Set'.inter_eq_right_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∩ s₂ = s₂ ↔ s₂ ⊆ s₁

source

theorem Set'.eq_of_subset_and_size_eq {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h₁ : s₁ ⊆ s₂) (h₂ : s₁.size = s₂.size) :

s₁ = s₂

source

theorem Set'.subset_of_size_inter_eq_size_left {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : (s₁ ∩ s₂).size = s₁.size) :

s₁ ⊆ s₂

source

theorem Set'.subset_of_size_inter_eq_size_right {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : (s₁ ∩ s₂).size = s₂.size) :

s₂ ⊆ s₁

source

@[simp]

theorem Set'.size_inter_eq_size_left_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(s₁ ∩ s₂).size = s₁.size ↔ s₁ ⊆ s₂

source

@[simp]

theorem Set'.size_inter_eq_size_right_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(s₁ ∩ s₂).size = s₂.size ↔ s₂ ⊆ s₁

source

@[simp]

theorem Set'.insert_subset_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

s₁.insert x ⊆ s₂ ↔ x ∈ s₂ ∧ s₁ ⊆ s₂

source

theorem Set'.diff_insert_eq_diff_erase {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

s₁ \ s₂.insert x = (s₁ \ s₂).erase x

source

theorem Set'.size_diff_add_eq_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ⊆ s₂) :

(s₂ \ s₁).size + s₁.size = s₂.size

source

theorem Set'.size_diff_eq_of_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ⊆ s₂) :

(s₂ \ s₁).size = s₂.size - s₁.size

source

def Set'.ssubset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s₁ s₂ : Set' α) :

Prop

Equations

s₁.ssubset s₂ = (s₁ ⊆ s₂ ∧ s₁ ≠ s₂)

Instances For

source

@[instance_reducible]

instance Set'.instHasSSubset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

HasSSubset (Set' α)

Equations

Set'.instHasSSubset = { SSubset := Set'.ssubset }

source

theorem Set'.ssubset_def {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ s₁ ≠ s₂

source

@[simp]

theorem Set'.union_eq_left_iff_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∪ s₂ = s₁ ↔ s₂ ⊆ s₁

source

@[simp]

theorem Set'.union_eq_right_iff_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ∪ s₂ = s₂ ↔ s₁ ⊆ s₂

source

theorem Set'.ssubset_iff_exi_disj_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ⊂ s₂ ↔ ∃ (s₃ : Set' α), s₃ ≠ ∅ ∧ (∀ x ∈ s₃, x ∉ s₁) ∧ s₁ ∪ s₃ = s₂

source

theorem Set'.insert_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

s₁.insert x ∪ s₂ = (s₁ ∪ s₂).insert x

source

theorem Set'.union_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} {x : α} :

s₁ ∪ s₂.insert x = (s₁ ∪ s₂).insert x

source

theorem Set'.size_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : ∀ x ∈ s₁, x ∉ s₂) :

(s₁ ∪ s₂).size = s₁.size + s₂.size

source

theorem Set'.size_union' {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : ∀ x ∈ s₂, x ∉ s₁) :

(s₁ ∪ s₂).size = s₁.size + s₂.size

source

@[simp]

theorem Set'.pos_size_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

0 < s.size ↔ s ≠ ∅

source

theorem Set'.size_lt_of_ssubset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h : s₁ ⊂ s₂) :

s₁.size < s₂.size

source

theorem Set'.eq_of_subset_and_subset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (h₁ : s₁ ⊆ s₂) (h₂ : s₂ ⊆ s₁) :

s₁ = s₂

source

theorem Set'.ssubset_iff_exi {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

s₁ ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ ∃ x ∈ s₂, x ∉ s₁

source

theorem Set'.diff_subset_of_right {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} (h₁ : s₂ ⊆ s₃) :

s₁ \ s₃ ⊆ s₁ \ s₂

source

theorem Set'.diff_ssubset_of_right {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ s₃ : Set' α} (h₁ : s₂ ⊆ s₃) (h₂ : ∃ x ∈ s₁, x ∈ s₃ ∧ x ∉ s₂) :

s₁ \ s₃ ⊂ s₁ \ s₂

source

noncomputable def Set'.compr {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (P : α → Prop) :

Set' α

Equations

Set'.compr P = Set'.ofSet (Set.ofPred P)

Instances For

source

def Set'.singleton {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (x : α) :

Set' α

Equations

Set'.singleton x = Set'.ofList [x]

Instances For

source

@[simp]

theorem Set'.mem_singleton {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x y : α} :

x ∈ singleton y ↔ x = y

source

@[simp]

theorem Set'.singleton_eq_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x y : α} :

singleton x = singleton y ↔ x = y

source

@[simp]

theorem Set'.singleton_ne_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

singleton x ≠ ∅

source

@[simp]

theorem Set'.size_singleton {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

(singleton x).size = 1

source

@[simp]

theorem Set'.empty_insert_eq_singleton {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

∅.insert x = singleton x

source

@[simp]

theorem Set'.toSet_singleton {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

(singleton x).toSet = {x}

source

@[simp]

theorem Set'.erase_singleton_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

(singleton x).erase x = ∅

source

@[simp]

theorem Set'.insert_singleton_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

(singleton x).insert x = singleton x

source

def Set'.toFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (s : Set' α) :

Finset α

Equations

s.toFinset = s.fold (fun (s₁ : Finset α) (x : α) => insert x s₁) ∅ ⋯

Instances For

source

@[simp]

theorem Set'.toFinset_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

∅.toFinset = ∅

source

theorem Set'.mem_toFinset_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} (hx : x ∈ s) :

x ∈ s.toFinset

source

@[simp]

theorem Set'.ofList_cons {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List α} {x : α} :

ofList (x :: xs) = (ofList xs).insert x

source

@[simp]

theorem Set'.ofList_append {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs ys : List α} :

ofList (xs ++ ys) = ofList xs ∪ ofList ys

source

theorem Set'.ind_ofList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {p : Set' α → Prop} (h : ∀ (xs : List α), xs.SortedLT → p (ofList xs)) (s : Set' α) :

p s

source

@[simp]

theorem Set'.sorted_toList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha : LinearOrder α] :

s.toList.SortedLT

source

theorem Set'.toList_ofList_of_nodup {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {xs : List α} (h : xs.Nodup) :

(ofList xs).toList = xs.mergeSort fun (a b : α) => decide (a ≤ b)

source

theorem Set'.toList_ofList_of_sortedLT {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {xs : List α} (h : xs.SortedLT) :

(ofList xs).toList = xs

source

theorem Set'.fold_insert {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {f : β → α → β} {z : β} {x : α} {hh : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x} (hx : x ∉ s) :

(s.insert x).fold f z hh = f (s.fold f z ⋯) x

source

@[simp]

theorem Set'.toFinset_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

(s.insert x).toFinset = insert x s.toFinset

source

@[simp]

theorem Set'.mem_toFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

x ∈ s.toFinset ↔ x ∈ s

source

theorem Set'.toSet_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(s₁ ∪ s₂).toSet = s₁.toSet ∪ s₂.toSet

source

theorem Set'.toSet_inter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(s₁ ∩ s₂).toSet = s₁.toSet ∩ s₂.toSet

source

theorem Set'.toFinset_union {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(s₁ ∪ s₂).toFinset = s₁.toFinset ∪ s₂.toFinset

source

theorem Set'.toFinset_inter {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} :

(s₁ ∩ s₂).toFinset = s₁.toFinset ∩ s₂.toFinset

source

@[simp]

theorem Set'.finite_toSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.toSet.Finite

source

@[simp]

theorem Set'.toFinset_coe_set {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

↑s.toFinset = s.toSet

source

@[simp]

theorem Set'.card_toFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.toFinset.card = s.size

source

@[simp]

theorem Set'.ncard_toSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.toSet.ncard = s.size

source

@[simp]

theorem Set'.ofSet_toSet_list {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List α} :

ofSet xs.toSet = ofList xs

source

@[simp]

theorem Set'.list_toSet_ofList {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {xs : List α} :

(ofList xs).toSet = xs.toSet

source

theorem Set'.ssubset_of {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s₁ s₂ : Set' α} (x : α) (h₁ : s₁ ⊆ s₂) (h₂ : x ∉ s₁) (h₃ : x ∈ s₂) :

s₁ ⊂ s₂

source

def Map.keysSet {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (mp : Map α β) :

Set' α

Equations

mp.keysSet = { inner := Std.ExtDHashMap.map (fun (x : α) (x_1 : β) => ()) mp.inner }

Instances For

source

@[simp]

theorem Map.mem_keysSet {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Map α β} {k : α} :

k ∈ mp.keysSet ↔ k ∈ mp

source

@[simp]

theorem Map.keySet_modify {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {mp : Map α β} {k : α} {f : β → β} :

(mp.modify k f).keysSet = mp.keysSet

source

@[simp]

theorem Set'.insert_erase_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

(s.erase x).insert x = s.insert x

source

@[simp]

theorem Set'.erase_insert_self {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

(s.insert x).erase x = s.erase x

source

@[simp]

theorem Set'.filter_eq_empty_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} :

s.filter p = ∅ ↔ ∀ x ∈ s, p x = false

source

@[simp]

theorem Set'.one_le_count_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {p : α → Bool} :

1 ≤ s.count p ↔ ∃ x ∈ s, p x = true

source

def Set'.bind {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] (s : Set' α) (f : α → Set' β) :

Set' β

Equations

s.bind f = s.fold (fun (s₁ : Set' β) (x : α) => s₁ ∪ f x) ∅ ⋯

Instances For

source

@[simp]

theorem Set'.bind_empty {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {f : α → Set' β} :

∅.bind f = ∅

source

theorem Set'.singleton_eq_insert {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {x : α} :

singleton x = ∅.insert x

source

@[simp]

theorem Set'.fold_singleton {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {f : β → α → β} {x : α} {z : β} {hh : ∀ {acc : β} {x y : α}, f (f acc x) y = f (f acc y) x} :

(singleton x).fold f z hh = f z x

source

@[simp]

theorem Set'.bind_singleton {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {f : α → Set' β} {x : α} :

(singleton x).bind f = f x

source

@[simp]

theorem Set'.bind_insert {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → Set' β} {x : α} :

(s.insert x).bind f = s.bind f ∪ f x

source

@[simp]

theorem Set'.mem_bind {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb₁ : DecidableEq β] [hb₂ : Hashable β] {s : Set' α} {f : α → Set' β} {y : β} :

y ∈ s.bind f ↔ ∃ x ∈ s, y ∈ f x

source

def Set'.head! {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (s : Set' α) :

Equations

s.head! = s.toList.head!

Instances For

source

def Set'.headMap! {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] [LinearOrder β] (s : Set' α) (f : α → β) :

Equations

s.headMap! f = (s.toList.mergeSort fun (x1 x2 : α) => decide (f x1 ≤ f x2)).head!

Instances For

source

theorem Set'.head!_spec {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] (h : s ≠ ∅) :

s.head! ∈ s ∧ ∀ x ∈ s, s.head! ≤ x

source

@[simp]

theorem Set'.head!_mem_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] :

s.head! ∈ s ↔ s ≠ ∅

source

theorem Set'.head!_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] (h : s ≠ ∅) :

s.head! ∈ s

source

theorem Set'.head!_le_of_mem {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] {x : α} (h : x ∈ s) :

s.head! ≤ x

source

theorem Set'.headMap!_spec {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] [hb : LinearOrder β] {f : α → β} (h : s ≠ ∅) :

s.headMap! f ∈ s ∧ ∀ x ∈ s, f (s.headMap! f) ≤ f x

source

@[simp]

theorem Set'.headMap!_mem_iff {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] [hb : LinearOrder β] {f : α → β} :

s.headMap! f ∈ s ↔ s ≠ ∅

source

theorem Set'.headMap!_mem {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] [hb : LinearOrder β] {f : α → β} (h : s ≠ ∅) :

s.headMap! f ∈ s

source

theorem Set'.headMap!_le_of_mem {α : Type u} {β : Type v} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} [ha₃ : Inhabited α] [ha₄ : LinearOrder α] [hb : LinearOrder β] {f : α → β} {x : α} (h : x ∈ s) :

f (s.headMap! f) ≤ f x

source

theorem Set'.size_eq_one_iff_singleton {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

s.size = 1 ↔ ∃ (x : α), s = singleton x

source

@[simp]

theorem Set'.ofFinset_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

ofFinset ∅ = ∅

source

@[simp]

theorem Set'.ofSet_empty {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] :

ofSet ∅ = ∅

source

@[simp]

theorem Set'.ofFinset_toFinset {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

ofFinset s.toFinset = s

source

@[simp]

theorem Set'.ofSet_toSet {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} :

ofSet s.toSet = s

source

theorem Set'.eq_singleton_iff_size {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

s = singleton x ↔ s.size = 1 ∧ x ∈ s

source

theorem Set'.singleton_eq_iff_size {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {s : Set' α} {x : α} :

singleton x = s ↔ s.size = 1 ∧ x ∈ s

source

@[simp]

theorem Set'.toList_ofList_eq_self_iff {α : Type u} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [ha : LinearOrder α] {xs : List α} :

(ofList xs).toList = xs ↔ xs.SortedLT