# Tree set lemmas #

This file contains lemmas about `Std.Data.TreeSet.Raw.Basic`. Most of the lemmas require `TransCmp cmp` for the comparison function `cmp`. These proofs can be obtained from `Std.Data.TreeSet.Raw.WF`.

source
@[simp]
theorem Std.TreeSet.Raw.isEmpty_emptyc {α : Type u} {cmp : α → α → Ordering} :
∅.isEmpty = true
source
@[simp]
theorem Std.TreeSet.Raw.isEmpty_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).isEmpty = false
source
theorem Std.TreeSet.Raw.mem_iff_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {k : α} :
k ∈ t ↔ t.contains k = true
source
@[simp]
theorem Std.TreeSet.Raw.contains_iff_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {k : α} :
t.contains k = true ↔ k ∈ t
source
theorem Std.TreeSet.Raw.contains_congr {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = Ordering.eq) :
t.contains k = t.contains k'
source
theorem Std.TreeSet.Raw.mem_congr {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = Ordering.eq) :
k ∈ t ↔ k' ∈ t
source
@[simp]
theorem Std.TreeSet.Raw.contains_emptyc {α : Type u} {cmp : α → α → Ordering} {k : α} :
∅.contains k = false
source
@[simp]
theorem Std.TreeSet.Raw.not_mem_emptyc {α : Type u} {cmp : α → α → Ordering} {k : α} :
¬k ∈ ∅
source
theorem Std.TreeSet.Raw.contains_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
t.isEmpty = true → t.contains a = false
source
theorem Std.TreeSet.Raw.not_mem_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
t.isEmpty = true → ¬a ∈ t
source
theorem Std.TreeSet.Raw.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.isEmpty = false ↔ ∃ (a : α), t.contains a = true
source
theorem Std.TreeSet.Raw.isEmpty_eq_false_iff_exists_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.isEmpty = false ↔ ∃ (a : α), a ∈ t
source
theorem Std.TreeSet.Raw.isEmpty_eq_false_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} (hc : t.contains a = true) :
t.isEmpty = false
source
theorem Std.TreeSet.Raw.isEmpty_iff_forall_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.isEmpty = true ↔ ∀ (a : α), t.contains a = false
source
theorem Std.TreeSet.Raw.isEmpty_iff_forall_not_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.isEmpty = true ↔ ∀ (a : α), ¬a ∈ t
source
@[simp]
theorem Std.TreeSet.Raw.insert_eq_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {p : α} :
Insert.insert p t = t.insert p
source
@[simp]
theorem Std.TreeSet.Raw.singleton_eq_insert {α : Type u} {cmp : α → α → Ordering} {p : α} :
{p} = ∅.insert p
source
@[simp]
theorem Std.TreeSet.Raw.contains_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [h : TransCmp cmp] :
t.WF → ∀ {k a : α}, (t.insert k).contains a = (cmp k a == Ordering.eq || t.contains a)
source
@[simp]
theorem Std.TreeSet.Raw.mem_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
a ∈ t.insert k ↔ cmp k a = Ordering.eq ∨ a ∈ t
source
theorem Std.TreeSet.Raw.contains_insert_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).contains k = true
source
theorem Std.TreeSet.Raw.mem_insert_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
k ∈ t.insert k
source
theorem Std.TreeSet.Raw.contains_of_contains_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
(t.insert k).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
source
theorem Std.TreeSet.Raw.mem_of_mem_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
a ∈ t.insert k → cmp k a ≠ Ordering.eq → a ∈ t
source
theorem Std.TreeSet.Raw.mem_of_mem_insert' {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
a ∈ t.insert k → ¬(cmp k a = Ordering.eq ∧ ¬k ∈ t) → a ∈ t

This is a restatement of `mem_of_mem_insert` that is written to exactly match the proof obligation in the statement of `get_insert`.

source
@[simp]
theorem Std.TreeSet.Raw.size_emptyc {α : Type u} {cmp : α → α → Ordering} :
∅.size = 0
source
theorem Std.TreeSet.Raw.isEmpty_eq_size_eq_zero {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} (h : t.WF) :
t.isEmpty = (t.size == 0)
source
theorem Std.TreeSet.Raw.size_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).size = if t.contains k = true then t.size else t.size + 1
source
theorem Std.TreeSet.Raw.size_le_size_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
t.size ≤ (t.insert k).size
source
theorem Std.TreeSet.Raw.size_insert_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).size ≤ t.size + 1
source
@[simp]
theorem Std.TreeSet.Raw.erase_emptyc {α : Type u} {cmp : α → α → Ordering} {k : α} :
∅.erase k = ∅
source
@[simp]
theorem Std.TreeSet.Raw.isEmpty_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
source
theorem Std.TreeSet.Raw.isEmpty_eq_isEmpty_erase_and_not_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (k : α) :
t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
source
theorem Std.TreeSet.Raw.isEmpty_eq_false_of_isEmpty_erase_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) :
t.isEmpty = false
source
@[simp]
theorem Std.TreeSet.Raw.contains_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
(t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
source
@[simp]
theorem Std.TreeSet.Raw.mem_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
source
theorem Std.TreeSet.Raw.contains_of_contains_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
(t.erase k).contains a = true → t.contains a = true
source
theorem Std.TreeSet.Raw.mem_of_mem_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
a ∈ t.erase k → a ∈ t
source
theorem Std.TreeSet.Raw.size_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.erase k).size = if t.contains k = true then t.size - 1 else t.size
source
theorem Std.TreeSet.Raw.size_erase_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.erase k).size ≤ t.size
source
theorem Std.TreeSet.Raw.size_le_size_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
t.size ≤ (t.erase k).size + 1
source
@[simp]
theorem Std.TreeSet.Raw.get?_emptyc {α : Type u} {cmp : α → α → Ordering} {a : α} :
∅.get? a = none
source
theorem Std.TreeSet.Raw.get?_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
t.isEmpty = true → t.get? a = none
source
theorem Std.TreeSet.Raw.get?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
(t.insert k).get? a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then some k else t.get? a
source
theorem Std.TreeSet.Raw.contains_eq_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = (t.get? a).isSome
source
@[simp]
theorem Std.TreeSet.Raw.isSome_get?_eq_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
(t.get? a).isSome = t.contains a
source
theorem Std.TreeSet.Raw.mem_iff_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
a ∈ t ↔ (t.get? a).isSome = true
source
@[simp]
theorem Std.TreeSet.Raw.isSome_get?_iff_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
(t.get? a).isSome = true ↔ a ∈ t
source
theorem Std.TreeSet.Raw.mem_of_get?_eq_some {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a a' : α} :
t.get? a = some a' → a' ∈ t
source
theorem Std.TreeSet.Raw.get?_eq_some_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k k' : α} :
t.get? k = some k' ↔ ∃ (h : k ∈ t), t.get k h = k'
source
theorem Std.TreeSet.Raw.get?_eq_none_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
t.contains a = false → t.get? a = none
source
theorem Std.TreeSet.Raw.get?_eq_none {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} :
¬a ∈ t → t.get? a = none
source
theorem Std.TreeSet.Raw.get?_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} :
(t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
source
@[simp]
theorem Std.TreeSet.Raw.get?_erase_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.erase k).get? k = none
source
theorem Std.TreeSet.Raw.compare_get?_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
Option.all (fun (x : α) => decide (cmp x k = Ordering.eq)) (t.get? k) = true
source
theorem Std.TreeSet.Raw.get?_congr {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k k' : α} (h' : cmp k k' = Ordering.eq) :
t.get? k = t.get? k'
source
theorem Std.TreeSet.Raw.get?_eq_some_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : t.contains k = true) :
t.get? k = some k
source
theorem Std.TreeSet.Raw.get?_eq_some {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t) :
t.get? k = some k
source
theorem Std.TreeSet.Raw.get_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} {h₁ : a ∈ t.insert k} :
(t.insert k).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.get a ⋯
source
@[simp]
theorem Std.TreeSet.Raw.get_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a : α} {h' : a ∈ t.erase k} :
(t.erase k).get a h' = t.get a ⋯
source
theorem Std.TreeSet.Raw.get?_eq_some_get {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} (h' : a ∈ t) :
t.get? a = some (t.get a h')
source
theorem Std.TreeSet.Raw.get_eq_get_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} {h' : a ∈ t} :
t.get a h' = (t.get? a).get ⋯
source
@[simp]
theorem Std.TreeSet.Raw.get_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} {h' : (t.get? a).isSome = true} :
(t.get? a).get h' = t.get a ⋯
source
theorem Std.TreeSet.Raw.compare_get_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t) :
cmp (t.get k h') k = Ordering.eq
source
theorem Std.TreeSet.Raw.get_congr {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t) :
t.get k₁ h₁ = t.get k₂ ⋯
source
@[simp]
theorem Std.TreeSet.Raw.get_eq {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t) :
t.get k h' = k
source
@[simp]
theorem Std.TreeSet.Raw.get!_emptyc {α : Type u} {cmp : α → α → Ordering} {a : α} [Inhabited α] :
∅.get! a = default
source
theorem Std.TreeSet.Raw.get!_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
t.isEmpty = true → t.get! a = default
source
theorem Std.TreeSet.Raw.get!_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} :
(t.insert k).get! a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.get! a
source
theorem Std.TreeSet.Raw.get!_eq_default_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
t.contains a = false → t.get! a = default
source
theorem Std.TreeSet.Raw.get!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
¬a ∈ t → t.get! a = default
source
theorem Std.TreeSet.Raw.get!_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} :
(t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
source
@[simp]
theorem Std.TreeSet.Raw.get!_erase_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
(t.erase k).get! k = default
source
theorem Std.TreeSet.Raw.get?_eq_some_get!_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
t.contains a = true → t.get? a = some (t.get! a)
source
theorem Std.TreeSet.Raw.get?_eq_some_get! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
a ∈ t → t.get? a = some (t.get! a)
source
theorem Std.TreeSet.Raw.get!_eq_get!_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
t.get! a = (t.get? a).get!
source
theorem Std.TreeSet.Raw.get_eq_get! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {h' : a ∈ t} :
t.get a h' = t.get! a
source
theorem Std.TreeSet.Raw.get!_congr {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k k' : α} (h' : cmp k k' = Ordering.eq) :
t.get! k = t.get! k'
source
theorem Std.TreeSet.Raw.get!_eq_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α} (h' : t.contains k = true) :
t.get! k = k
source
theorem Std.TreeSet.Raw.get!_eq_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α} (h' : k ∈ t) :
t.get! k = k
source
@[simp]
theorem Std.TreeSet.Raw.getD_emptyc {α : Type u} {cmp : α → α → Ordering} {a fallback : α} :
∅.getD a fallback = fallback
source
theorem Std.TreeSet.Raw.getD_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} :
t.isEmpty = true → t.getD a fallback = fallback
source
theorem Std.TreeSet.Raw.getD_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a fallback : α} :
(t.insert k).getD a fallback = if cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.getD a fallback
source
theorem Std.TreeSet.Raw.getD_eq_fallback_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} :
t.contains a = false → t.getD a fallback = fallback
source
theorem Std.TreeSet.Raw.getD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} :
¬a ∈ t → t.getD a fallback = fallback
source
theorem Std.TreeSet.Raw.getD_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k a fallback : α} :
(t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
source
@[simp]
theorem Std.TreeSet.Raw.getD_erase_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} :
(t.erase k).getD k fallback = fallback
source
theorem Std.TreeSet.Raw.get?_eq_some_getD_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} :
t.contains a = true → t.get? a = some (t.getD a fallback)
source
theorem Std.TreeSet.Raw.get?_eq_some_getD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} :
a ∈ t → t.get? a = some (t.getD a fallback)
source
theorem Std.TreeSet.Raw.getD_eq_getD_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} :
t.getD a fallback = (t.get? a).getD fallback
source
theorem Std.TreeSet.Raw.get_eq_getD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} {h' : a ∈ t} :
t.get a h' = t.getD a fallback
source
theorem Std.TreeSet.Raw.get!_eq_getD_default {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} :
t.get! a = t.getD a default
source
theorem Std.TreeSet.Raw.getD_congr {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k k' fallback : α} (h' : cmp k k' = Ordering.eq) :
t.getD k fallback = t.getD k' fallback
source
theorem Std.TreeSet.Raw.getD_eq_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k fallback : α} (h' : t.contains k = true) :
t.getD k fallback = k
source
theorem Std.TreeSet.Raw.getD_eq_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k fallback : α} (h' : k ∈ t) :
t.getD k fallback = k
source
@[simp]
theorem Std.TreeSet.Raw.containsThenInsert_fst {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.containsThenInsert k).fst = t.contains k
source
@[simp]
theorem Std.TreeSet.Raw.containsThenInsert_snd {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.containsThenInsert k).snd = t.insert k
source
@[simp]
theorem Std.TreeSet.Raw.length_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.toList.length = t.size
source
@[simp]
theorem Std.TreeSet.Raw.isEmpty_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} :
t.toList.isEmpty = t.isEmpty
source
@[simp]
theorem Std.TreeSet.Raw.contains_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
t.toList.contains k = t.contains k
source
@[simp]
theorem Std.TreeSet.Raw.mem_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
k ∈ t.toList ↔ k ∈ t
source
theorem Std.TreeSet.Raw.mem_of_mem_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
k ∈ t.toList → k ∈ t
source
theorem Std.TreeSet.Raw.distinct_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.toList
source
theorem Std.TreeSet.Raw.ordered_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.toList
source
theorem Std.TreeSet.Raw.foldlM_eq_foldlM_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
foldlM f init t = List.foldlM f init t.toList
source
theorem Std.TreeSet.Raw.foldl_eq_foldl_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {f : δ → α → δ} {init : δ} :
foldl f init t = List.foldl f init t.toList
source
theorem Std.TreeSet.Raw.foldrM_eq_foldrM_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
foldrM f init t = List.foldrM f init t.toList
source
theorem Std.TreeSet.Raw.foldr_eq_foldr_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {f : α → δ → δ} {init : δ} :
foldr f init t = List.foldr f init t.toList
source
theorem Std.TreeSet.Raw.forM_eq_forM_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → m PUnit} :
ForM.forM t f = t.toList.forM f
source
theorem Std.TreeSet.Raw.forIn_eq_forIn_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
ForIn.forIn t init f = ForIn.forIn t.toList init f
source
@[simp]
theorem Std.TreeSet.Raw.insertMany_nil {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} :
t.insertMany [] = t
source
@[simp]
theorem Std.TreeSet.Raw.insertMany_list_singleton {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {k : α} :
t.insertMany [k] = t.insert k
source
theorem Std.TreeSet.Raw.insertMany_cons {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {l : List α} {k : α} :
t.insertMany (k :: l) = (t.insert k).insertMany l
source
theorem Std.TreeSet.Raw.insertMany_append {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {l₁ l₂ : List α} :
t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
source
@[simp]
theorem Std.TreeSet.Raw.contains_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} :
(t.insertMany l).contains k = (t.contains k || l.contains k)
source
@[simp]
theorem Std.TreeSet.Raw.mem_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} :
k ∈ t.insertMany l ↔ k ∈ t ∨ l.contains k = true
source
theorem Std.TreeSet.Raw.mem_of_mem_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ t.insertMany l → k ∈ t
source
theorem Std.TreeSet.Raw.get?_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) :
(t.insertMany l).get? k = none
source
theorem Std.TreeSet.Raw.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(t.insertMany l).get? k' = some k
source
theorem Std.TreeSet.Raw.get?_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k : α} (mem : k ∈ t) :
(t.insertMany l).get? k = t.get? k
source
theorem Std.TreeSet.Raw.get_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k : α} {h' : k ∈ t.insertMany l} (contains : k ∈ t) :
(t.insertMany l).get k h' = t.get k contains
source
theorem Std.TreeSet.Raw.get_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {h' : k' ∈ t.insertMany l} (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(t.insertMany l).get k' h' = k
source
theorem Std.TreeSet.Raw.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) :
(t.insertMany l).get! k = default
source
theorem Std.TreeSet.Raw.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(t.insertMany l).get! k' = k
source
theorem Std.TreeSet.Raw.get!_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α} (mem : k ∈ t) :
(t.insertMany l).get! k = t.get! k
source
theorem Std.TreeSet.Raw.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k fallback : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) :
(t.insertMany l).getD k fallback = fallback
source
theorem Std.TreeSet.Raw.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(t.insertMany l).getD k' fallback = k
source
theorem Std.TreeSet.Raw.getD_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k fallback : α} (mem : k ∈ t) :
(t.insertMany l).getD k fallback = t.getD k fallback
source
theorem Std.TreeSet.Raw.size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) :
(∀ (a : α), a ∈ t → l.contains a = false) → (t.insertMany l).size = t.size + l.length
source
theorem Std.TreeSet.Raw.size_le_size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} :
t.size ≤ (t.insertMany l).size
source
theorem Std.TreeSet.Raw.size_insertMany_list_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} :
(t.insertMany l).size ≤ t.size + l.length
source
@[simp]
theorem Std.TreeSet.Raw.isEmpty_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {l : List α} :
(t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
source
@[simp]
theorem Std.TreeSet.Raw.ofList_nil {α : Type u} {cmp : α → α → Ordering} :
ofList [] cmp = ∅
source
@[simp]
theorem Std.TreeSet.Raw.ofList_singleton {α : Type u} {cmp : α → α → Ordering} {k : α} :
ofList [k] cmp = ∅.insert k
source
theorem Std.TreeSet.Raw.ofList_cons {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α} :
ofList (hd :: tl) cmp = (∅.insert hd).insertMany tl
source
theorem Std.TreeSet.Raw.ofList_eq_insertMany_empty {α : Type u} {cmp : α → α → Ordering} {l : List α} :
ofList l cmp = ∅.insertMany l
source
@[simp]
theorem Std.TreeSet.Raw.contains_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
(ofList l cmp).contains k = l.contains k
source
@[simp]
theorem Std.TreeSet.Raw.mem_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
k ∈ ofList l cmp ↔ l.contains k = true
source
theorem Std.TreeSet.Raw.get?_ofList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
(ofList l cmp).get? k = none
source
theorem Std.TreeSet.Raw.get?_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(ofList l cmp).get? k' = some k
source
theorem Std.TreeSet.Raw.get_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) {h' : k' ∈ ofList l cmp} :
(ofList l cmp).get k' h' = k
source
theorem Std.TreeSet.Raw.get!_ofList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
(ofList l cmp).get! k = default
source
theorem Std.TreeSet.Raw.get!_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(ofList l cmp).get! k' = k
source
theorem Std.TreeSet.Raw.getD_ofList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :
(ofList l cmp).getD k fallback = fallback
source
theorem Std.TreeSet.Raw.getD_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
(ofList l cmp).getD k' fallback = k
source
theorem Std.TreeSet.Raw.size_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) :
(ofList l cmp).size = l.length
source
theorem Std.TreeSet.Raw.size_ofList_le {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
(ofList l cmp).size ≤ l.length
source
@[simp]
theorem Std.TreeSet.Raw.isEmpty_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
(ofList l cmp).isEmpty = l.isEmpty
source
@[simp]
theorem Std.TreeSet.Raw.min?_emptyc {α : Type u} {cmp : α → α → Ordering} :
empty.min? = none
source
theorem Std.TreeSet.Raw.min?_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) :
t.min? = none
source
@[simp]
theorem Std.TreeSet.Raw.min?_eq_none_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.min? = none ↔ t.isEmpty = true
source
theorem Std.TreeSet.Raw.min?_eq_some_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} :
t.min? = some km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.min?_eq_some_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km : α} :
t.min? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
@[simp]
theorem Std.TreeSet.Raw.isNone_min?_eq_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.min?.isNone = t.isEmpty
source
@[simp]
theorem Std.TreeSet.Raw.isSome_min?_eq_not_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.min?.isSome = !t.isEmpty
source
theorem Std.TreeSet.Raw.isSome_min?_iff_isEmpty_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.min?.isSome = true ↔ t.isEmpty = false
source
theorem Std.TreeSet.Raw.min?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).min? = some (t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k')
source
theorem Std.TreeSet.Raw.isSome_min?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).min?.isSome = true
source
theorem Std.TreeSet.Raw.min?_insert_le_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km kmi : α} (hkm : t.min? = some km) (hkmi : (t.insert k).min?.get ⋯ = kmi) :
(cmp kmi km).isLE = true
source
theorem Std.TreeSet.Raw.min?_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k kmi : α} (hkmi : (t.insert k).min?.get ⋯ = kmi) :
(cmp kmi k).isLE = true
source
theorem Std.TreeSet.Raw.contains_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.min? = some km) :
t.contains km = true
source
theorem Std.TreeSet.Raw.isSome_min?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) :
t.min?.isSome = true
source
theorem Std.TreeSet.Raw.isSome_min?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
k ∈ t → t.min?.isSome = true
source
theorem Std.TreeSet.Raw.min?_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : t.contains k = true) (hkm : t.min?.get ⋯ = km) :
(cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.min?_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : k ∈ t) (hkm : t.min?.get ⋯ = km) :
(cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.le_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {k : α} (h : t.WF) :
(∀ (k' : α), t.min? = some k' → (cmp k k').isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
theorem Std.TreeSet.Raw.get?_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.min? = some km) :
t.get? km = some km
source
theorem Std.TreeSet.Raw.get_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} {hc : t.contains km = true} (hkm : t.min?.get ⋯ = km) :
t.get km hc = km
source
theorem Std.TreeSet.Raw.get!_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {km : α} (hkm : t.min? = some km) :
t.get! km = km
source
theorem Std.TreeSet.Raw.getD_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km fallback : α} (hkm : t.min? = some km) :
t.getD km fallback = km
source
@[simp]
theorem Std.TreeSet.Raw.min?_bind_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.min?.bind t.get? = t.min?
source
theorem Std.TreeSet.Raw.min?_erase_eq_iff_not_compare_eq_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.erase k).min? = t.min? ↔ ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq
source
theorem Std.TreeSet.Raw.min?_erase_eq_of_not_compare_eq_min? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq) :
(t.erase k).min? = t.min?
source
theorem Std.TreeSet.Raw.isSome_min?_of_isSome_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hs : (t.erase k).min?.isSome = true) :
t.min?.isSome = true
source
theorem Std.TreeSet.Raw.min?_le_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km kme : α} (hkme : (t.erase k).min? = some kme) (hkm : t.min?.get ⋯ = km) :
(cmp km kme).isLE = true
source
theorem Std.TreeSet.Raw.min?_eq_head?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.min? = t.toList.head?
source
theorem Std.TreeSet.Raw.min?_eq_some_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.min? = some t.min!
source
theorem Std.TreeSet.Raw.min!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = true) :
t.min! = default
source
theorem Std.TreeSet.Raw.min!_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} :
t.min! = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.min!_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} :
t.min! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.min!_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
(t.insert k).min! = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
source
theorem Std.TreeSet.Raw.min!_insert_le_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} :
(cmp (t.insert k).min! t.min!).isLE = true
source
theorem Std.TreeSet.Raw.min!_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
(cmp (t.insert k).min! k).isLE = true
source
theorem Std.TreeSet.Raw.contains_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.contains t.min! = true
source
theorem Std.TreeSet.Raw.min!_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.min! ∈ t
source
theorem Std.TreeSet.Raw.min!_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : t.contains k = true) :
(cmp t.min! k).isLE = true
source
theorem Std.TreeSet.Raw.min!_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : k ∈ t) :
(cmp t.min! k).isLE = true
source
theorem Std.TreeSet.Raw.le_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} :
(cmp k t.min!).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
theorem Std.TreeSet.Raw.get?_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.get? t.min! = some t.min!
source
theorem Std.TreeSet.Raw.get_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {hc : t.min! ∈ t} :
t.get t.min! hc = t.min!
source
theorem Std.TreeSet.Raw.get!_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.get! t.min! = t.min!
source
theorem Std.TreeSet.Raw.getD_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.getD t.min! fallback = t.min!
source
theorem Std.TreeSet.Raw.min!_erase_eq_of_not_compare_min!_eq {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k t.min! = Ordering.eq) :
(t.erase k).min! = t.min!
source
theorem Std.TreeSet.Raw.min!_le_min!_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) :
(cmp t.min! (t.erase k).min!).isLE = true
source
theorem Std.TreeSet.Raw.min!_eq_head!_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.min! = t.toList.head!
source
theorem Std.TreeSet.Raw.min?_eq_some_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.min? = some (t.minD fallback)
source
theorem Std.TreeSet.Raw.minD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) {fallback : α} :
t.minD fallback = fallback
source
theorem Std.TreeSet.Raw.min!_eq_minD_default {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.min! = t.minD default
source
theorem Std.TreeSet.Raw.minD_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback : α} :
t.minD fallback = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.minD_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback : α} :
t.minD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.TreeSet.Raw.minD_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} :
(t.insert k).minD fallback = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
source
theorem Std.TreeSet.Raw.minD_insert_le_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback : α} :
(cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.minD_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} :
(cmp ((t.insert k).minD fallback) k).isLE = true
source
theorem Std.TreeSet.Raw.contains_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.contains (t.minD fallback) = true
source
theorem Std.TreeSet.Raw.minD_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.minD fallback ∈ t
source
theorem Std.TreeSet.Raw.minD_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) {fallback : α} :
(cmp (t.minD fallback) k).isLE = true
source
theorem Std.TreeSet.Raw.minD_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : k ∈ t) {fallback : α} :
(cmp (t.minD fallback) k).isLE = true
source
theorem Std.TreeSet.Raw.le_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback : α} :
(cmp k (t.minD fallback)).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
theorem Std.TreeSet.Raw.get?_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.get? (t.minD fallback) = some (t.minD fallback)
source
theorem Std.TreeSet.Raw.get_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {fallback : α} {hc : t.minD fallback ∈ t} :
t.get (t.minD fallback) hc = t.minD fallback
source
theorem Std.TreeSet.Raw.get!_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.get! (t.minD fallback) = t.minD fallback
source
theorem Std.TreeSet.Raw.getD_minD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback' : α} :
t.getD (t.minD fallback) fallback' = t.minD fallback
source
theorem Std.TreeSet.Raw.minD_erase_eq_of_not_compare_minD_eq {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k (t.minD fallback) = Ordering.eq) :
(t.erase k).minD fallback = t.minD fallback
source
theorem Std.TreeSet.Raw.minD_le_minD_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) {fallback : α} :
(cmp (t.minD fallback) ((t.erase k).minD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.minD_eq_headD_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {fallback : α} :
t.minD fallback = t.toList.headD fallback
source
@[simp]
theorem Std.TreeSet.Raw.max?_emptyc {α : Type u} {cmp : α → α → Ordering} :
empty.max? = none
source
theorem Std.TreeSet.Raw.max?_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) :
t.max? = none
source
@[simp]
theorem Std.TreeSet.Raw.max?_eq_none_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max? = none ↔ t.isEmpty = true
source
theorem Std.TreeSet.Raw.max?_eq_some_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} :
t.max? = some km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.max?_eq_some_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km : α} :
t.max? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
@[simp]
theorem Std.TreeSet.Raw.isNone_max?_eq_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max?.isNone = t.isEmpty
source
@[simp]
theorem Std.TreeSet.Raw.isSome_max?_eq_not_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max?.isSome = !t.isEmpty
source
theorem Std.TreeSet.Raw.isSome_max?_iff_isEmpty_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max?.isSome = true ↔ t.isEmpty = false
source
theorem Std.TreeSet.Raw.max?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).max? = some (t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k')
source
theorem Std.TreeSet.Raw.isSome_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.insert k).max?.isSome = true
source
theorem Std.TreeSet.Raw.max?_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km kmi : α} (hkm : t.max? = some km) (hkmi : (t.insert k).max?.get ⋯ = kmi) :
(cmp km kmi).isLE = true
source
theorem Std.TreeSet.Raw.self_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k kmi : α} (hkmi : (t.insert k).max?.get ⋯ = kmi) :
(cmp k kmi).isLE = true
source
theorem Std.TreeSet.Raw.contains_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.max? = some km) :
t.contains km = true
source
theorem Std.TreeSet.Raw.isSome_max?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) :
t.max?.isSome = true
source
theorem Std.TreeSet.Raw.isSome_max?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
k ∈ t → t.max?.isSome = true
source
theorem Std.TreeSet.Raw.le_max?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : t.contains k = true) (hkm : t.max?.get ⋯ = km) :
(cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.le_max?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : k ∈ t) (hkm : t.max?.get ⋯ = km) :
(cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.max?_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {k : α} (h : t.WF) :
(∀ (k' : α), t.max? = some k' → (cmp k' k).isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
theorem Std.TreeSet.Raw.get?_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.max? = some km) :
t.get? km = some km
source
theorem Std.TreeSet.Raw.get_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km : α} {hc : t.contains km = true} (hkm : t.max?.get ⋯ = km) :
t.get km hc = km
source
theorem Std.TreeSet.Raw.get!_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {km : α} (hkm : t.max? = some km) :
t.get! km = km
source
theorem Std.TreeSet.Raw.getD_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {km fallback : α} (hkm : t.max? = some km) :
t.getD km fallback = km
source
@[simp]
theorem Std.TreeSet.Raw.max?_bind_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max?.bind t.get? = t.max?
source
theorem Std.TreeSet.Raw.max?_erase_eq_iff_not_compare_eq_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} :
(t.erase k).max? = t.max? ↔ ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq
source
theorem Std.TreeSet.Raw.max?_erase_eq_of_not_compare_eq_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq) :
(t.erase k).max? = t.max?
source
theorem Std.TreeSet.Raw.isSome_max?_of_isSome_max?_erase {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hs : (t.erase k).max?.isSome = true) :
t.max?.isSome = true
source
theorem Std.TreeSet.Raw.max?_erase_le_max? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k km kme : α} (hkme : (t.erase k).max? = some kme) (hkm : t.max?.get ⋯ = km) :
(cmp kme km).isLE = true
source
theorem Std.TreeSet.Raw.max?_eq_getLast?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max? = t.toList.getLast?
source
@[deprecated Std.TreeSet.Raw.max?_eq_getLast?_toList (since := "2025-05-23")]
theorem Std.TreeSet.Raw.max?_eq_head?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) :
t.max? = t.toList.getLast?
source
theorem Std.TreeSet.Raw.max?_eq_some_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.max? = some t.max!
source
theorem Std.TreeSet.Raw.max!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = true) :
t.max! = default
source
theorem Std.TreeSet.Raw.max!_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} :
t.max! = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.max!_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} :
t.max! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.max!_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
(t.insert k).max! = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
source
theorem Std.TreeSet.Raw.max!_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} :
(cmp t.max! (t.insert k).max!).isLE = true
source
theorem Std.TreeSet.Raw.self_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} :
(cmp k (t.insert k).max!).isLE = true
source
theorem Std.TreeSet.Raw.contains_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.contains t.max! = true
source
theorem Std.TreeSet.Raw.max!_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.max! ∈ t
source
theorem Std.TreeSet.Raw.le_max!_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : t.contains k = true) :
(cmp k t.max!).isLE = true
source
theorem Std.TreeSet.Raw.le_max!_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : k ∈ t) :
(cmp k t.max!).isLE = true
source
theorem Std.TreeSet.Raw.max!_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} :
(cmp t.max! k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
theorem Std.TreeSet.Raw.get?_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.get? t.max! = some t.max!
source
theorem Std.TreeSet.Raw.get_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {hc : t.max! ∈ t} :
t.get t.max! hc = t.max!
source
theorem Std.TreeSet.Raw.get!_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.get! t.max! = t.max!
source
theorem Std.TreeSet.Raw.getD_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.getD t.max! fallback = t.max!
source
theorem Std.TreeSet.Raw.max!_erase_eq_of_not_compare_max!_eq {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k t.max! = Ordering.eq) :
(t.erase k).max! = t.max!
source
theorem Std.TreeSet.Raw.max!_erase_le_max! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) :
(cmp (t.erase k).max! t.max!).isLE = true
source
theorem Std.TreeSet.Raw.max!_eq_getLast!_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.max! = t.toList.getLast!
source
theorem Std.TreeSet.Raw.max?_eq_some_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.max? = some (t.maxD fallback)
source
theorem Std.TreeSet.Raw.maxD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) {fallback : α} :
t.maxD fallback = fallback
source
theorem Std.TreeSet.Raw.max!_eq_maxD_default {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.max! = t.maxD default
source
theorem Std.TreeSet.Raw.maxD_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback : α} :
t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.maxD_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback : α} :
t.maxD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.TreeSet.Raw.maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} :
(t.insert k).maxD fallback = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
source
theorem Std.TreeSet.Raw.maxD_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback : α} :
(cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.self_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} :
(cmp k ((t.insert k).maxD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.contains_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.contains (t.maxD fallback) = true
source
theorem Std.TreeSet.Raw.maxD_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.maxD fallback ∈ t
source
theorem Std.TreeSet.Raw.le_maxD_of_contains {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) {fallback : α} :
(cmp k (t.maxD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.le_maxD_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : k ∈ t) {fallback : α} :
(cmp k (t.maxD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.maxD_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback : α} :
(cmp (t.maxD fallback) k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
theorem Std.TreeSet.Raw.get?_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.get? (t.maxD fallback) = some (t.maxD fallback)
source
theorem Std.TreeSet.Raw.get_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {fallback : α} {hc : t.maxD fallback ∈ t} :
t.get (t.maxD fallback) hc = t.maxD fallback
source
theorem Std.TreeSet.Raw.get!_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} :
t.get! (t.maxD fallback) = t.maxD fallback
source
theorem Std.TreeSet.Raw.getD_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback' : α} :
t.getD (t.maxD fallback) fallback' = t.maxD fallback
source
theorem Std.TreeSet.Raw.maxD_erase_eq_of_not_compare_maxD_eq {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k (t.maxD fallback) = Ordering.eq) :
(t.erase k).maxD fallback = t.maxD fallback
source
theorem Std.TreeSet.Raw.maxD_erase_le_maxD {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) {fallback : α} :
(cmp ((t.erase k).maxD fallback) (t.maxD fallback)).isLE = true
source
theorem Std.TreeSet.Raw.maxD_eq_getLastD_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {fallback : α} :
t.maxD fallback = t.toList.getLastD fallback
source
@[simp]
theorem Std.TreeSet.Raw.Equiv.rfl {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} :
t.Equiv t
source
theorem Std.TreeSet.Raw.Equiv.symm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} :
t₁.Equiv t₂ → t₂.Equiv t₁
source
theorem Std.TreeSet.Raw.Equiv.trans {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} :
t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃
source
instance Std.TreeSet.Raw.Equiv.instTrans {α : Type u} {cmp : α → α → Ordering} :
Trans Equiv Equiv Equiv
Equations

- Std.TreeSet.Raw.Equiv.instTrans = { trans := ⋯ }

source
theorem Std.TreeSet.Raw.Equiv.comm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} :
t₁.Equiv t₂ ↔ t₂.Equiv t₁
source
theorem Std.TreeSet.Raw.Equiv.congr_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} (h : t₁.Equiv t₂) :
t₁.Equiv t₃ ↔ t₂.Equiv t₃
source
theorem Std.TreeSet.Raw.Equiv.congr_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} (h : t₁.Equiv t₂) :
t₃.Equiv t₁ ↔ t₃.Equiv t₂
source
theorem Std.TreeSet.Raw.Equiv.isEmpty_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h : t₁.Equiv t₂) :
t₁.isEmpty = t₂.isEmpty
source
theorem Std.TreeSet.Raw.Equiv.contains_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.contains k = t₂.contains k
source
theorem Std.TreeSet.Raw.Equiv.mem_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
k ∈ t₁ ↔ k ∈ t₂
source
theorem Std.TreeSet.Raw.Equiv.size_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.size = t₂.size
source
theorem Std.TreeSet.Raw.Equiv.get?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.get? k = t₂.get? k
source
theorem Std.TreeSet.Raw.Equiv.getKey_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.get k hk = t₂.get k ⋯
source
theorem Std.TreeSet.Raw.Equiv.getKey!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.get! k = t₂.get! k
source
theorem Std.TreeSet.Raw.Equiv.getKeyD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getD k fallback = t₂.getD k fallback
source
theorem Std.TreeSet.Raw.Equiv.toList_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.toList = t₂.toList
source
theorem Std.TreeSet.Raw.Equiv.toArray_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.toArray = t₂.toArray
source
theorem Std.TreeSet.Raw.Equiv.foldlM_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
foldlM f init t₁ = foldlM f init t₂
source
theorem Std.TreeSet.Raw.Equiv.foldl_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} [TransCmp cmp] {f : δ → α → δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
foldl f init t₁ = foldl f init t₂
source
theorem Std.TreeSet.Raw.Equiv.foldrM_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
foldrM f init t₁ = foldrM f init t₂
source
theorem Std.TreeSet.Raw.Equiv.foldr_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} [TransCmp cmp] {f : α → δ → δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
foldr f init t₁ = foldr f init t₂
source
theorem Std.TreeSet.Raw.Equiv.forIn_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {b : δ} {f : α → δ → m (ForInStep δ)} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
ForIn.forIn t₁ b f = ForIn.forIn t₂ b f
source
theorem Std.TreeSet.Raw.Equiv.forM_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
ForM.forM t₁ f = ForM.forM t₂ f
source
theorem Std.TreeSet.Raw.Equiv.any_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {p : α → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.any p = t₂.any p
source
theorem Std.TreeSet.Raw.Equiv.all_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {p : α → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.all p = t₂.all p
source
theorem Std.TreeSet.Raw.Equiv.min?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.min? = t₂.min?
source
theorem Std.TreeSet.Raw.Equiv.min!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.min! = t₂.min!
source
theorem Std.TreeSet.Raw.Equiv.minD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.minD fallback = t₂.minD fallback
source
theorem Std.TreeSet.Raw.Equiv.max?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.max? = t₂.max?
source
theorem Std.TreeSet.Raw.Equiv.max!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.max! = t₂.max!
source
theorem Std.TreeSet.Raw.Equiv.maxD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.maxD fallback = t₂.maxD fallback
source
theorem Std.TreeSet.Raw.Equiv.atIdx?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {i : Nat} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.atIdx? i = t₂.atIdx? i
source
theorem Std.TreeSet.Raw.Equiv.atIdx!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {i : Nat} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.atIdx! i = t₂.atIdx! i
source
theorem Std.TreeSet.Raw.Equiv.atIdxD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {i : Nat} {fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.atIdxD i fallback = t₂.atIdxD i fallback
source
theorem Std.TreeSet.Raw.Equiv.getGE?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getGE? k = t₂.getGE? k
source
theorem Std.TreeSet.Raw.Equiv.getGE!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getGE! k = t₂.getGE! k
source
theorem Std.TreeSet.Raw.Equiv.getGED_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getGED k fallback = t₂.getGED k fallback
source
theorem Std.TreeSet.Raw.Equiv.getGT?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getGT? k = t₂.getGT? k
source
theorem Std.TreeSet.Raw.Equiv.getGT!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getGT! k = t₂.getGT! k
source
theorem Std.TreeSet.Raw.Equiv.getGTD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getGTD k fallback = t₂.getGTD k fallback
source
theorem Std.TreeSet.Raw.Equiv.getLE?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getLE? k = t₂.getLE? k
source
theorem Std.TreeSet.Raw.Equiv.getLE!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getLE! k = t₂.getLE! k
source
theorem Std.TreeSet.Raw.Equiv.getLED_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getLED k fallback = t₂.getLED k fallback
source
theorem Std.TreeSet.Raw.Equiv.getLT?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getLT? k = t₂.getLT? k
source
theorem Std.TreeSet.Raw.Equiv.getLT!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getLT! k = t₂.getLT! k
source
theorem Std.TreeSet.Raw.Equiv.getLTD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) :
t₁.getLTD k fallback = t₂.getLTD k fallback
source
theorem Std.TreeSet.Raw.Equiv.insert {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (k : α) :
(t₁.insert k).Equiv (t₂.insert k)
source
theorem Std.TreeSet.Raw.Equiv.erase {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (k : α) :
(t₁.erase k).Equiv (t₂.erase k)
source
theorem Std.TreeSet.Raw.Equiv.filter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (f : α → Bool) :
(Raw.filter f t₁).Equiv (Raw.filter f t₂)
source
theorem Std.TreeSet.Raw.Equiv.insertMany_list {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (l : List α) :
(t₁.insertMany l).Equiv (t₂.insertMany l)
source
theorem Std.TreeSet.Raw.Equiv.eraseMany_list {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (l : List α) :
(t₁.eraseMany l).Equiv (t₂.eraseMany l)
source
theorem Std.TreeSet.Raw.Equiv.merge {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) :
(t₁.merge t₃).Equiv (t₂.merge t₄)
source
theorem Std.TreeSet.Raw.Equiv.of_forall_get?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (k : α), t₁.get? k = t₂.get? k) :
t₁.Equiv t₂
source
theorem Std.TreeSet.Raw.Equiv.of_forall_contains_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (k : α), t₁.contains k = t₂.contains k) :
t₁.Equiv t₂
source
theorem Std.TreeSet.Raw.Equiv.of_forall_mem_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) :
t₁.Equiv t₂
source
theorem Std.TreeSet.Raw.equiv_empty_iff_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} :
t.Equiv empty ↔ t.isEmpty = true
source
theorem Std.TreeSet.Raw.empty_equiv_iff_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} :
empty.Equiv t ↔ t.isEmpty = true
source
theorem Std.TreeSet.Raw.equiv_iff_toList_perm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} :
t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
source
theorem Std.TreeSet.Raw.Equiv.of_toList_perm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h : t₁.toList.Perm t₂.toList) :
t₁.Equiv t₂
source
theorem Std.TreeSet.Raw.equiv_iff_toList_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
t₁.Equiv t₂ ↔ t₁.toList = t₂.toList
source
theorem Std.TreeSet.Raw.toList_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {f : α → Bool} (h : t.WF) :
(filter f t).toList = List.filter f t.toList
source
theorem Std.TreeSet.Raw.isEmpty_filter_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) :
(filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = false
source
theorem Std.TreeSet.Raw.isEmpty_filter_eq_false_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) :
(filter f t).isEmpty = false ↔ ∃ (k : α), ∃ (h : k ∈ t), f (t.get k h) = true
source
@[simp]
theorem Std.TreeSet.Raw.mem_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} (h : t.WF) :
k ∈ filter f t ↔ ∃ (h' : k ∈ t), f (t.get k h') = true
source
theorem Std.TreeSet.Raw.mem_of_mem_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} (h : t.WF) :
k ∈ filter f t → k ∈ t
source
theorem Std.TreeSet.Raw.size_filter_le_size {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) :
(filter f t).size ≤ t.size
source
theorem Std.TreeSet.Raw.size_filter_eq_size_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) :
(filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
source
theorem Std.TreeSet.Raw.filter_equiv_self_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) :
(filter f t).Equiv t ↔ ∀ (a : α) (h : a ∈ t), f (t.get a h) = true
source
@[simp]
theorem Std.TreeSet.Raw.get?_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} (h : t.WF) :
(filter f t).get? k = Option.filter f (t.get? k)
source
@[simp]
theorem Std.TreeSet.Raw.get_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} {h' : k ∈ filter f t} (h : t.WF) :
(filter f t).get k h' = t.get k ⋯
source
theorem Std.TreeSet.Raw.get!_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] {f : α → Bool} {k : α} (h : t.WF) :
(filter f t).get! k = (Option.filter f (t.get? k)).get!
source
theorem Std.TreeSet.Raw.getD_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k fallback : α} (h : t.WF) :
(filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback