Documentation

Std.Data.TreeSet.Raw.WF

Well-formedness proofs for raw tree sets #

This file contains well-formedness proofs about Std.Data.TreeSet.Raw.Basic. Most of the lemmas require TransCmp cmp for the comparison function cmp.

theorem Std.TreeSet.Raw.WF.empty {α : Type u} {cmp : α → α → Ordering} :

theorem Std.TreeSet.Raw.WF.emptyc {α : Type u} {cmp : α → α → Ordering} :

theorem Std.TreeSet.Raw.WF.erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {a : α} (h : t.WF) :

(t.erase a).WF

theorem Std.TreeSet.Raw.WF.insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {a : α} (h : t.WF) :

(t.insert a).WF

theorem Std.TreeSet.Raw.WF.containsThenInsert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {a : α} (h : t.WF) :

(t.containsThenInsert a).snd.WF

theorem Std.TreeSet.Raw.WF.filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) :

(Raw.filter f t).WF

theorem Std.TreeSet.Raw.WF.partition_fst {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} :

(partition f t).fst.WF

theorem Std.TreeSet.Raw.WF.partition_snd {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} :

(partition f t).snd.WF

theorem Std.TreeSet.Raw.WF.eraseMany {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α cmp} (h : t.WF) :

(t.eraseMany l).WF

theorem Std.TreeSet.Raw.WF.insertMany {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Raw α cmp} (h : t.WF) :

(t.insertMany l).WF

theorem Std.TreeSet.Raw.WF.ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :

(Raw.ofList l cmp).WF

theorem Std.TreeSet.Raw.WF.ofArray {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a : Array α} :

(Raw.ofArray a cmp).WF

theorem Std.TreeSet.Raw.WF.merge {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h : t₁.WF) :

(t₁.merge t₂).WF

theorem Std.TreeSet.Raw.WF.union {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) :

(t₁ ∪ t₂).WF

theorem Std.TreeSet.Raw.WF.inter {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) :

(t₁ ∩ t₂).WF

theorem Std.TreeSet.Raw.WF.diff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) :

(t₁ \ t₂).WF