# Tree set lemmas #

This file contains lemmas about `Std.ExtTreeSet`.

source
@[simp]
theorem Std.ExtTreeSet.isEmpty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.isEmpty = true ↔ t = ∅
source
@[simp]
theorem Std.ExtTreeSet.isEmpty_eq_false_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.isEmpty = false ↔ ¬t = ∅
source
@[simp]
theorem Std.ExtTreeSet.isEmpty_empty {α : Type u} {cmp : α → α → Ordering} :
∅.isEmpty = true
source
@[simp]
theorem Std.ExtTreeSet.empty_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} :
∅ = t ↔ t = ∅
source
@[simp]
theorem Std.ExtTreeSet.insert_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
t.insert k ≠ ∅
source
theorem Std.ExtTreeSet.mem_iff_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
k ∈ t ↔ t.contains k = true
source
@[simp]
theorem Std.ExtTreeSet.contains_iff_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
t.contains k = true ↔ k ∈ t
source
theorem Std.ExtTreeSet.contains_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (hab : cmp k k' = Ordering.eq) :
t.contains k = t.contains k'
source
theorem Std.ExtTreeSet.mem_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (hab : cmp k k' = Ordering.eq) :
k ∈ t ↔ k' ∈ t
source
@[simp]
theorem Std.ExtTreeSet.contains_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} :
∅.contains k = false
source
@[simp]
theorem Std.ExtTreeSet.not_mem_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} :
¬k ∈ ∅
source
theorem Std.ExtTreeSet.eq_empty_iff_forall_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t = ∅ ↔ ∀ (a : α), t.contains a = false
source
theorem Std.ExtTreeSet.eq_empty_iff_forall_not_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t = ∅ ↔ ∀ (a : α), ¬a ∈ t
source
theorem Std.ExtTreeSet.ne_empty_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} (h : a ∈ t) :
t ≠ ∅
source
@[simp]
theorem Std.ExtTreeSet.insert_eq_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {p : α} :
Insert.insert p t = t.insert p
source
@[simp]
theorem Std.ExtTreeSet.singleton_eq_insert {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {p : α} :
{p} = ∅.insert p
source
@[simp]
theorem Std.ExtTreeSet.contains_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
(t.insert k).contains a = (cmp k a == Ordering.eq || t.contains a)
source
@[simp]
theorem Std.ExtTreeSet.mem_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
a ∈ t.insert k ↔ cmp k a = Ordering.eq ∨ a ∈ t
source
theorem Std.ExtTreeSet.contains_insert_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).contains k = true
source
theorem Std.ExtTreeSet.mem_insert_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
k ∈ t.insert k
source
theorem Std.ExtTreeSet.contains_of_contains_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
(t.insert k).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true
source
theorem Std.ExtTreeSet.mem_of_mem_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
a ∈ t.insert k → cmp k a ≠ Ordering.eq → a ∈ t
source
theorem Std.ExtTreeSet.mem_of_mem_insert' {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.size_empty {α : Type u} {cmp : α → α → Ordering} :
∅.size = 0
source
theorem Std.ExtTreeSet.isEmpty_eq_size_beq_zero {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} :
t.isEmpty = (t.size == 0)
source
theorem Std.ExtTreeSet.eq_empty_iff_size_eq_zero {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t = ∅ ↔ t.size = 0
source
theorem Std.ExtTreeSet.size_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).size = if t.contains k = true then t.size else t.size + 1
source
theorem Std.ExtTreeSet.size_le_size_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
t.size ≤ (t.insert k).size
source
theorem Std.ExtTreeSet.size_insert_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).size ≤ t.size + 1
source
@[simp]
theorem Std.ExtTreeSet.erase_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} :
∅.erase k = ∅
source
@[simp]
theorem Std.ExtTreeSet.erase_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
t.erase k = ∅ ↔ t = ∅ ∨ t.size = 1 ∧ k ∈ t
source
theorem Std.ExtTreeSet.eq_empty_iff_erase_eq_empty_and_not_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (k : α) :
t = ∅ ↔ t.erase k = ∅ ∧ ¬k ∈ t
source
theorem Std.ExtTreeSet.ne_empty_of_erase_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (h : t.erase k ≠ ∅) :
t ≠ ∅
source
@[simp]
theorem Std.ExtTreeSet.contains_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
(t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
source
@[simp]
theorem Std.ExtTreeSet.mem_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t
source
theorem Std.ExtTreeSet.contains_of_contains_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
(t.erase k).contains a = true → t.contains a = true
source
theorem Std.ExtTreeSet.mem_of_mem_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
(t.erase k).contains a = true → t.contains a = true
source
theorem Std.ExtTreeSet.size_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.erase k).size = if t.contains k = true then t.size - 1 else t.size
source
theorem Std.ExtTreeSet.size_erase_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.erase k).size ≤ t.size
source
theorem Std.ExtTreeSet.size_le_size_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
t.size ≤ (t.erase k).size + 1
source
@[simp]
theorem Std.ExtTreeSet.get?_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a : α} :
∅.get? a = none
source
theorem Std.ExtTreeSet.get?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.contains_eq_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} :
t.contains a = (t.get? a).isSome
source
@[simp]
theorem Std.ExtTreeSet.isSome_get?_eq_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} :
(t.get? a).isSome = t.contains a
source
theorem Std.ExtTreeSet.mem_iff_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} :
a ∈ t ↔ (t.get? a).isSome = true
source
@[simp]
theorem Std.ExtTreeSet.isSome_get?_iff_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} :
(t.get? a).isSome = true ↔ a ∈ t
source
theorem Std.ExtTreeSet.mem_of_get?_eq_some {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (h : t.get? k = some k') :
k' ∈ t
source
theorem Std.ExtTreeSet.get?_eq_some_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} :
t.get? k = some k' ↔ ∃ (h : k ∈ t), t.get k h = k'
source
theorem Std.ExtTreeSet.get?_eq_none_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} :
t.contains a = false → t.get? a = none
source
theorem Std.ExtTreeSet.get?_eq_none {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} :
¬a ∈ t → t.get? a = none
source
theorem Std.ExtTreeSet.get?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} :
(t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
source
@[simp]
theorem Std.ExtTreeSet.get?_erase_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.erase k).get? k = none
source
theorem Std.ExtTreeSet.compare_get?_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
Option.all (fun (x : α) => decide (cmp x k = Ordering.eq)) (t.get? k) = true
source
theorem Std.ExtTreeSet.get?_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (h' : cmp k k' = Ordering.eq) :
t.get? k = t.get? k'
source
theorem Std.ExtTreeSet.get?_eq_some_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : t.contains k = true) :
t.get? k = some k
source
theorem Std.ExtTreeSet.get?_eq_some {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k ∈ t) :
t.get? k = some k
source
theorem Std.ExtTreeSet.get_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.get_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} {h' : a ∈ t.erase k} :
(t.erase k).get a h' = t.get a ⋯
source
theorem Std.ExtTreeSet.get?_eq_some_get {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} (h' : a ∈ t) :
t.get? a = some (t.get a h')
source
theorem Std.ExtTreeSet.get_eq_get_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {h : k ∈ t} :
t.get k h = (t.get? k).get ⋯
source
theorem Std.ExtTreeSet.get_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {h : (t.get? k).isSome = true} :
(t.get? k).get h = t.get k ⋯
source
theorem Std.ExtTreeSet.compare_get_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (h' : k ∈ t) :
cmp (t.get k h') k = Ordering.eq
source
theorem Std.ExtTreeSet.get_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t) :
t.get k₁ h₁ = t.get k₂ ⋯
source
@[simp]
theorem Std.ExtTreeSet.get_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k ∈ t) :
t.get k h' = k
source
@[simp]
theorem Std.ExtTreeSet.get!_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] {a : α} :
∅.get! a = default
source
theorem Std.ExtTreeSet.get!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k a : α} :
(t.insert k).get! a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.get! a
source
theorem Std.ExtTreeSet.get!_eq_default_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} :
t.contains a = false → t.get! a = default
source
theorem Std.ExtTreeSet.get!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} :
¬a ∈ t → t.get! a = default
source
theorem Std.ExtTreeSet.get!_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k a : α} :
(t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
source
@[simp]
theorem Std.ExtTreeSet.get!_erase_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} :
(t.erase k).get! k = default
source
theorem Std.ExtTreeSet.get?_eq_some_get!_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} :
t.contains a = true → t.get? a = some (t.get! a)
source
theorem Std.ExtTreeSet.get?_eq_some_get! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} :
a ∈ t → t.get? a = some (t.get! a)
source
theorem Std.ExtTreeSet.get!_eq_get!_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} :
t.get! a = (t.get? a).get!
source
theorem Std.ExtTreeSet.get_eq_get! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} {h : a ∈ t} :
t.get a h = t.get! a
source
theorem Std.ExtTreeSet.get!_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k k' : α} (h' : cmp k k' = Ordering.eq) :
t.get! k = t.get! k'
source
theorem Std.ExtTreeSet.get!_eq_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : t.contains k = true) :
t.get! k = k
source
theorem Std.ExtTreeSet.get!_eq_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : k ∈ t) :
t.get! k = k
source
@[simp]
theorem Std.ExtTreeSet.getD_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a fallback : α} :
∅.getD a fallback = fallback
source
theorem Std.ExtTreeSet.getD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.getD_eq_fallback_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} :
t.contains a = false → t.getD a fallback = fallback
source
theorem Std.ExtTreeSet.getD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} :
¬a ∈ t → t.getD a fallback = fallback
source
theorem Std.ExtTreeSet.getD_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.getD_erase_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} :
(t.erase k).getD k fallback = fallback
source
theorem Std.ExtTreeSet.get?_eq_some_getD_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} :
t.contains a = true → t.get? a = some (t.getD a fallback)
source
theorem Std.ExtTreeSet.get?_eq_some_getD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} :
a ∈ t → t.get? a = some (t.getD a fallback)
source
theorem Std.ExtTreeSet.getD_eq_getD_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} :
t.getD a fallback = (t.get? a).getD fallback
source
theorem Std.ExtTreeSet.get_eq_getD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} {h : a ∈ t} :
t.get a h = t.getD a fallback
source
theorem Std.ExtTreeSet.get!_eq_getD_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} :
t.get! a = t.getD a default
source
theorem Std.ExtTreeSet.getD_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' fallback : α} (h' : cmp k k' = Ordering.eq) :
t.getD k fallback = t.getD k' fallback
source
theorem Std.ExtTreeSet.getD_eq_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : t.contains k = true) :
t.getD k fallback = k
source
theorem Std.ExtTreeSet.getD_eq_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : k ∈ t) :
t.getD k fallback = k
source
@[simp]
theorem Std.ExtTreeSet.containsThenInsert_fst {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.containsThenInsert k).fst = t.contains k
source
@[simp]
theorem Std.ExtTreeSet.containsThenInsert_snd {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.containsThenInsert k).snd = t.insert k
source
@[simp]
theorem Std.ExtTreeSet.length_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.toList.length = t.size
source
@[simp]
theorem Std.ExtTreeSet.isEmpty_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.toList.isEmpty = t.isEmpty
source
@[simp]
theorem Std.ExtTreeSet.toList_eq_nil_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.toList = [] ↔ t = ∅
source
@[simp]
theorem Std.ExtTreeSet.contains_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
t.toList.contains k = t.contains k
source
@[simp]
theorem Std.ExtTreeSet.mem_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
k ∈ t.toList ↔ k ∈ t
source
theorem Std.ExtTreeSet.distinct_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.toList
source
theorem Std.ExtTreeSet.ordered_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.toList
source
theorem Std.ExtTreeSet.foldlM_eq_foldlM_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
foldlM f init t = List.foldlM f init t.toList
source
theorem Std.ExtTreeSet.foldl_eq_foldl_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} [TransCmp cmp] {f : δ → α → δ} {init : δ} :
foldl f init t = List.foldl f init t.toList
source
theorem Std.ExtTreeSet.foldrM_eq_foldrM_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
foldrM f init t = List.foldrM f init t.toList
source
theorem Std.ExtTreeSet.foldr_eq_foldr_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} [TransCmp cmp] {f : α → δ → δ} {init : δ} :
foldr f init t = List.foldr f init t.toList
source
@[simp]
theorem Std.ExtTreeSet.forM_eq_forM {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} :
forM f t = ForM.forM t f
source
theorem Std.ExtTreeSet.forM_eq_forM_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} :
ForM.forM t f = t.toList.forM f
source
@[simp]
theorem Std.ExtTreeSet.forIn_eq_forIn {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
forIn f init t = ForIn.forIn t init f
source
theorem Std.ExtTreeSet.forIn_eq_forIn_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
ForIn.forIn t init f = ForIn.forIn t.toList init f
source
@[simp]
theorem Std.ExtTreeSet.insertMany_nil {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.insertMany [] = t
source
@[simp]
theorem Std.ExtTreeSet.insertMany_list_singleton {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
t.insertMany [k] = t.insert k
source
theorem Std.ExtTreeSet.insertMany_cons {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} :
t.insertMany (k :: l) = (t.insert k).insertMany l
source
theorem Std.ExtTreeSet.insertMany_append {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l₁ l₂ : List α} :
t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
source
@[simp]
theorem Std.ExtTreeSet.contains_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
(t.insertMany l).contains k = (t.contains k || l.contains k)
source
@[simp]
theorem Std.ExtTreeSet.mem_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
k ∈ t.insertMany l ↔ k ∈ t ∨ l.contains k = true
source
theorem Std.ExtTreeSet.mem_of_mem_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ t.insertMany l → k ∈ t
source
theorem Std.ExtTreeSet.get?_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) :
(t.insertMany l).get? k = none
source
theorem Std.ExtTreeSet.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.get?_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} (mem : k ∈ t) :
(t.insertMany l).get? k = t.get? k
source
theorem Std.ExtTreeSet.get_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} {h' : k ∈ t.insertMany l} (contains : k ∈ t) :
(t.insertMany l).get k h' = t.get k contains
source
theorem Std.ExtTreeSet.get_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) :
(t.insertMany l).get! k = default
source
theorem Std.ExtTreeSet.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {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.ExtTreeSet.get!_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {l : List α} {k : α} (mem : k ∈ t) :
(t.insertMany l).get! k = t.get! k
source
theorem Std.ExtTreeSet.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {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.ExtTreeSet.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.getD_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k fallback : α} (mem : k ∈ t) :
(t.insertMany l).getD k fallback = t.getD k fallback
source
theorem Std.ExtTreeSet.size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {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.ExtTreeSet.size_le_size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} :
t.size ≤ (t.insertMany l).size
source
theorem Std.ExtTreeSet.size_insertMany_list_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} :
(t.insertMany l).size ≤ t.size + l.length
source
@[simp]
theorem Std.ExtTreeSet.isEmpty_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} :
(t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
source
@[simp]
theorem Std.ExtTreeSet.insertMany_list_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} :
t.insertMany l = ∅ ↔ t = ∅ ∧ l = []
source
@[simp]
theorem Std.ExtTreeSet.ofList_nil {α : Type u} {cmp : α → α → Ordering} :
ofList [] cmp = ∅
source
@[simp]
theorem Std.ExtTreeSet.ofList_singleton {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} :
ofList [k] cmp = ∅.insert k
source
theorem Std.ExtTreeSet.ofList_cons {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {hd : α} {tl : List α} :
ofList (hd :: tl) cmp = (∅.insert hd).insertMany tl
source
theorem Std.ExtTreeSet.ofList_eq_insertMany_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
ofList l cmp = ∅.insertMany l
source
@[simp]
theorem Std.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.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.ExtTreeSet.size_ofList_le {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
(ofList l cmp).size ≤ l.length
source
@[simp]
theorem Std.ExtTreeSet.ofList_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
ofList l cmp = ∅ ↔ l = []
source
@[simp]
theorem Std.ExtTreeSet.min?_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] :
∅.min? = none
source
@[simp]
theorem Std.ExtTreeSet.min?_eq_none_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.min? = none ↔ t = ∅
source
theorem Std.ExtTreeSet.min?_eq_some_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} :
t.min? = some km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.min?_eq_some_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {km : α} :
t.min? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
@[simp]
theorem Std.ExtTreeSet.isNone_min?_eq_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.min?.isNone = t.isEmpty
source
@[simp]
theorem Std.ExtTreeSet.isSome_min?_eq_not_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.min?.isSome = !t.isEmpty
source
theorem Std.ExtTreeSet.isSome_min?_iff_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.min?.isSome = true ↔ t ≠ ∅
source
theorem Std.ExtTreeSet.min?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.isSome_min?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).min?.isSome = true
source
theorem Std.ExtTreeSet.min?_insert_le_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kmi : α} (hkm : t.min? = some km) (hkmi : (t.insert k).min?.get ⋯ = kmi) :
(cmp kmi km).isLE = true
source
theorem Std.ExtTreeSet.min?_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k kmi : α} (hkmi : (t.insert k).min?.get ⋯ = kmi) :
(cmp kmi k).isLE = true
source
theorem Std.ExtTreeSet.contains_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.min? = some km) :
t.contains km = true
source
theorem Std.ExtTreeSet.min?_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.min? = some km) :
km ∈ t
source
theorem Std.ExtTreeSet.isSome_min?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
t.min?.isSome = true
source
theorem Std.ExtTreeSet.isSome_min?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
k ∈ t → t.min?.isSome = true
source
theorem Std.ExtTreeSet.min?_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : t.contains k = true) (hkm : t.min?.get ⋯ = km) :
(cmp km k).isLE = true
source
theorem Std.ExtTreeSet.min?_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : k ∈ t) (hkm : t.min?.get ⋯ = km) :
(cmp km k).isLE = true
source
theorem Std.ExtTreeSet.le_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(∀ (k' : α), t.min? = some k' → (cmp k k').isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
theorem Std.ExtTreeSet.get?_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.min? = some km) :
t.get? km = some km
source
theorem Std.ExtTreeSet.get_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} {hc : t.contains km = true} (hkm : t.min?.get ⋯ = km) :
t.get km hc = km
source
theorem Std.ExtTreeSet.get!_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {km : α} (hkm : t.min? = some km) :
t.get! km = km
source
theorem Std.ExtTreeSet.getD_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km fallback : α} (hkm : t.min? = some km) :
t.getD km fallback = km
source
@[simp]
theorem Std.ExtTreeSet.min?_bind_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.min?.bind t.get? = t.min?
source
theorem Std.ExtTreeSet.min?_erase_eq_iff_not_compare_eq_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.erase k).min? = t.min? ↔ ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq
source
theorem Std.ExtTreeSet.min?_erase_eq_of_not_compare_eq_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq) :
(t.erase k).min? = t.min?
source
theorem Std.ExtTreeSet.isSome_min?_of_isSome_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hs : (t.erase k).min?.isSome = true) :
t.min?.isSome = true
source
theorem Std.ExtTreeSet.min?_le_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kme : α} (hkme : (t.erase k).min? = some kme) (hkm : t.min?.get ⋯ = km) :
(cmp km kme).isLE = true
source
theorem Std.ExtTreeSet.min?_eq_head?_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.min? = t.toList.head?
source
theorem Std.ExtTreeSet.min_eq_get_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.min he = t.min?.get ⋯
source
theorem Std.ExtTreeSet.min?_eq_some_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) :
t.min? = some (t.min he)
source
theorem Std.ExtTreeSet.min_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {km : α} :
t.min he = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.min_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {he : t ≠ ∅} {km : α} :
t.min he = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.min_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).min ⋯ = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
source
theorem Std.ExtTreeSet.min_insert_le_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} :
(cmp ((t.insert k).min ⋯) (t.min he)).isLE = true
source
theorem Std.ExtTreeSet.min_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(cmp ((t.insert k).min ⋯) k).isLE = true
source
theorem Std.ExtTreeSet.contains_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.contains (t.min he) = true
source
theorem Std.ExtTreeSet.min_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.min he ∈ t
source
theorem Std.ExtTreeSet.min_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
(cmp (t.min ⋯) k).isLE = true
source
theorem Std.ExtTreeSet.min_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) :
(cmp (t.min ⋯) k).isLE = true
source
theorem Std.ExtTreeSet.le_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} :
(cmp k (t.min he)).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
@[simp]
theorem Std.ExtTreeSet.get?_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.get? (t.min he) = some (t.min he)
source
@[simp]
theorem Std.ExtTreeSet.get_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {hc : t.min he ∈ t} :
t.get (t.min he) hc = t.min he
source
@[simp]
theorem Std.ExtTreeSet.get!_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} :
t.get! (t.min he) = t.min he
source
@[simp]
theorem Std.ExtTreeSet.getD_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {fallback : α} :
t.getD (t.min he) fallback = t.min he
source
@[simp]
theorem Std.ExtTreeSet.min_erase_eq_iff_not_compare_eq_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} :
(t.erase k).min he = t.min ⋯ ↔ ¬cmp k (t.min ⋯) = Ordering.eq
source
theorem Std.ExtTreeSet.min_erase_eq_of_not_compare_eq_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} (hc : ¬cmp k (t.min ⋯) = Ordering.eq) :
(t.erase k).min he = t.min ⋯
source
theorem Std.ExtTreeSet.min_le_min_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} :
(cmp (t.min ⋯) ((t.erase k).min he)).isLE = true
source
theorem Std.ExtTreeSet.min_eq_head_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.min he = t.toList.head ⋯
source
theorem Std.ExtTreeSet.min?_eq_some_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.min? = some t.min!
source
theorem Std.ExtTreeSet.min_eq_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} :
t.min he = t.min!
source
theorem Std.ExtTreeSet.min!_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] :
∅.min! = default
source
theorem Std.ExtTreeSet.min!_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} :
t.min! = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.min!_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} :
t.min! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.min!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} :
(t.insert k).min! = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
source
theorem Std.ExtTreeSet.min!_insert_le_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} :
(cmp (t.insert k).min! t.min!).isLE = true
source
theorem Std.ExtTreeSet.min!_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} :
(cmp (t.insert k).min! k).isLE = true
source
theorem Std.ExtTreeSet.contains_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.contains t.min! = true
source
theorem Std.ExtTreeSet.min!_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.min! ∈ t
source
theorem Std.ExtTreeSet.min!_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : t.contains k = true) :
(cmp t.min! k).isLE = true
source
theorem Std.ExtTreeSet.min!_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : k ∈ t) :
(cmp t.min! k).isLE = true
source
theorem Std.ExtTreeSet.le_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} :
(cmp k t.min!).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
theorem Std.ExtTreeSet.get?_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.get? t.min! = some t.min!
source
theorem Std.ExtTreeSet.get_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.min! ∈ t} :
t.get t.min! hc = t.min!
source
@[simp]
theorem Std.ExtTreeSet.get_min!_eq_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.min! ∈ t} :
t.get t.min! hc = t.min ⋯
source
theorem Std.ExtTreeSet.get!_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.get! t.min! = t.min!
source
theorem Std.ExtTreeSet.getD_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} :
t.getD t.min! fallback = t.min!
source
theorem Std.ExtTreeSet.min!_erase_eq_of_not_compare_min!_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k t.min! = Ordering.eq) :
(t.erase k).min! = t.min!
source
theorem Std.ExtTreeSet.min!_le_min!_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) :
(cmp t.min! (t.erase k).min!).isLE = true
source
theorem Std.ExtTreeSet.min!_eq_head!_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] :
t.min! = t.toList.head!
source
theorem Std.ExtTreeSet.min?_eq_some_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.min? = some (t.minD fallback)
source
theorem Std.ExtTreeSet.minD_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {fallback : α} :
∅.minD fallback = fallback
source
theorem Std.ExtTreeSet.min!_eq_minD_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] :
t.min! = t.minD default
source
theorem Std.ExtTreeSet.minD_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {km fallback : α} :
t.minD fallback = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.minD_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (he : t ≠ ∅) {km fallback : α} :
t.minD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true
source
theorem Std.ExtTreeSet.minD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.minD_insert_le_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} :
(cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true
source
theorem Std.ExtTreeSet.minD_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} :
(cmp ((t.insert k).minD fallback) k).isLE = true
source
theorem Std.ExtTreeSet.contains_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.contains (t.minD fallback) = true
source
theorem Std.ExtTreeSet.minD_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.minD fallback ∈ t
source
theorem Std.ExtTreeSet.minD_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) {fallback : α} :
(cmp (t.minD fallback) k).isLE = true
source
theorem Std.ExtTreeSet.minD_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) {fallback : α} :
(cmp (t.minD fallback) k).isLE = true
source
theorem Std.ExtTreeSet.le_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} :
(cmp k (t.minD fallback)).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true
source
theorem Std.ExtTreeSet.get?_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.get? (t.minD fallback) = some (t.minD fallback)
source
theorem Std.ExtTreeSet.get_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} {hc : t.minD fallback ∈ t} :
t.get (t.minD fallback) hc = t.minD fallback
source
theorem Std.ExtTreeSet.get!_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} :
t.get! (t.minD fallback) = t.minD fallback
source
theorem Std.ExtTreeSet.getD_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback fallback' : α} :
t.getD (t.minD fallback) fallback' = t.minD fallback
source
theorem Std.ExtTreeSet.minD_erase_eq_of_not_compare_minD_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k (t.minD fallback) = Ordering.eq) :
(t.erase k).minD fallback = t.minD fallback
source
theorem Std.ExtTreeSet.minD_le_minD_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (he : t.erase k ≠ ∅) {fallback : α} :
(cmp (t.minD fallback) ((t.erase k).minD fallback)).isLE = true
source
theorem Std.ExtTreeSet.minD_eq_headD_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} :
t.minD fallback = t.toList.headD fallback
source
@[simp]
theorem Std.ExtTreeSet.max?_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] :
∅.max? = none
source
@[simp]
theorem Std.ExtTreeSet.max?_eq_none_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.max? = none ↔ t = ∅
source
theorem Std.ExtTreeSet.max?_eq_some_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} :
t.max? = some km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.max?_eq_some_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {km : α} :
t.max? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
@[simp]
theorem Std.ExtTreeSet.isNone_max?_eq_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.max?.isNone = t.isEmpty
source
@[simp]
theorem Std.ExtTreeSet.isSome_max?_eq_not_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.max?.isSome = !t.isEmpty
source
theorem Std.ExtTreeSet.isSome_max?_iff_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.max?.isSome = true ↔ t ≠ ∅
source
theorem Std.ExtTreeSet.max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.isSome_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).max?.isSome = true
source
theorem Std.ExtTreeSet.max?_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kmi : α} (hkm : t.max? = some km) (hkmi : (t.insert k).max?.get ⋯ = kmi) :
(cmp km kmi).isLE = true
source
theorem Std.ExtTreeSet.self_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k kmi : α} (hkmi : (t.insert k).max?.get ⋯ = kmi) :
(cmp k kmi).isLE = true
source
theorem Std.ExtTreeSet.contains_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.max? = some km) :
t.contains km = true
source
theorem Std.ExtTreeSet.max?_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.max? = some km) :
km ∈ t
source
theorem Std.ExtTreeSet.isSome_max?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
t.max?.isSome = true
source
theorem Std.ExtTreeSet.isSome_max?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
k ∈ t → t.max?.isSome = true
source
theorem Std.ExtTreeSet.le_max?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : t.contains k = true) (hkm : t.max?.get ⋯ = km) :
(cmp k km).isLE = true
source
theorem Std.ExtTreeSet.le_max?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : k ∈ t) (hkm : t.max?.get ⋯ = km) :
(cmp k km).isLE = true
source
theorem Std.ExtTreeSet.max?_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(∀ (k' : α), t.max? = some k' → (cmp k' k).isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
theorem Std.ExtTreeSet.get?_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.max? = some km) :
t.get? km = some km
source
theorem Std.ExtTreeSet.get_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} {hc : t.contains km = true} (hkm : t.max?.get ⋯ = km) :
t.get km hc = km
source
theorem Std.ExtTreeSet.get!_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {km : α} (hkm : t.max? = some km) :
t.get! km = km
source
theorem Std.ExtTreeSet.getD_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km fallback : α} (hkm : t.max? = some km) :
t.getD km fallback = km
source
@[simp]
theorem Std.ExtTreeSet.max?_bind_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.max?.bind t.get? = t.max?
source
theorem Std.ExtTreeSet.max?_erase_eq_iff_not_compare_eq_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.erase k).max? = t.max? ↔ ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq
source
theorem Std.ExtTreeSet.max?_erase_eq_of_not_compare_eq_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq) :
(t.erase k).max? = t.max?
source
theorem Std.ExtTreeSet.isSome_max?_of_isSome_max?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hs : (t.erase k).max?.isSome = true) :
t.max?.isSome = true
source
theorem Std.ExtTreeSet.max?_erase_le_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kme : α} (hkme : (t.erase k).max? = some kme) (hkm : t.max?.get ⋯ = km) :
(cmp kme km).isLE = true
source
theorem Std.ExtTreeSet.max?_eq_getLast?_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] :
t.max? = t.toList.getLast?
source
theorem Std.ExtTreeSet.max_eq_get_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.max he = t.max?.get ⋯
source
theorem Std.ExtTreeSet.max?_eq_some_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) :
t.max? = some (t.max he)
source
theorem Std.ExtTreeSet.max_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {km : α} :
t.max he = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.max_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {he : t ≠ ∅} {km : α} :
t.max he = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.max_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(t.insert k).max ⋯ = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
source
theorem Std.ExtTreeSet.max_le_max_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} :
(cmp (t.max he) ((t.insert k).max ⋯)).isLE = true
source
theorem Std.ExtTreeSet.self_le_max_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} :
(cmp k ((t.insert k).max ⋯)).isLE = true
source
theorem Std.ExtTreeSet.contains_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.contains (t.max he) = true
source
theorem Std.ExtTreeSet.max_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.max he ∈ t
source
theorem Std.ExtTreeSet.le_max_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
(cmp k (t.max ⋯)).isLE = true
source
theorem Std.ExtTreeSet.le_max_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) :
(cmp k (t.max ⋯)).isLE = true
source
theorem Std.ExtTreeSet.max_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} :
(cmp (t.max he) k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
@[simp]
theorem Std.ExtTreeSet.get?_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.get? (t.max he) = some (t.max he)
source
@[simp]
theorem Std.ExtTreeSet.get_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {hc : t.max he ∈ t} :
t.get (t.max he) hc = t.max he
source
@[simp]
theorem Std.ExtTreeSet.get!_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} :
t.get! (t.max he) = t.max he
source
@[simp]
theorem Std.ExtTreeSet.getD_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {fallback : α} :
t.getD (t.max he) fallback = t.max he
source
@[simp]
theorem Std.ExtTreeSet.max_erase_eq_iff_not_compare_eq_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} :
(t.erase k).max he = t.max ⋯ ↔ ¬cmp k (t.max ⋯) = Ordering.eq
source
theorem Std.ExtTreeSet.max_erase_eq_of_not_compare_eq_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} (hc : ¬cmp k (t.max ⋯) = Ordering.eq) :
(t.erase k).max he = t.max ⋯
source
theorem Std.ExtTreeSet.max_erase_le_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} :
(cmp ((t.erase k).max he) (t.max ⋯)).isLE = true
source
theorem Std.ExtTreeSet.max_eq_getLast_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} :
t.max he = t.toList.getLast ⋯
source
theorem Std.ExtTreeSet.max?_eq_some_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.max? = some t.max!
source
theorem Std.ExtTreeSet.max_eq_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} :
t.max he = t.max!
source
theorem Std.ExtTreeSet.max!_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] :
∅.max! = default
source
theorem Std.ExtTreeSet.max!_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} :
t.max! = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.max!_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} :
t.max! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.max!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} :
(t.insert k).max! = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
source
theorem Std.ExtTreeSet.max!_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} :
(cmp t.max! (t.insert k).max!).isLE = true
source
theorem Std.ExtTreeSet.self_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} :
(cmp k (t.insert k).max!).isLE = true
source
theorem Std.ExtTreeSet.contains_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.contains t.max! = true
source
theorem Std.ExtTreeSet.max!_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.max! ∈ t
source
theorem Std.ExtTreeSet.le_max!_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : t.contains k = true) :
(cmp k t.max!).isLE = true
source
theorem Std.ExtTreeSet.le_max!_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : k ∈ t) :
(cmp k t.max!).isLE = true
source
theorem Std.ExtTreeSet.max!_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} :
(cmp t.max! k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
theorem Std.ExtTreeSet.get?_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.get? t.max! = some t.max!
source
theorem Std.ExtTreeSet.get_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.max! ∈ t} :
t.get t.max! hc = t.max!
source
@[simp]
theorem Std.ExtTreeSet.get_max!_eq_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.max! ∈ t} :
t.get t.max! hc = t.max ⋯
source
theorem Std.ExtTreeSet.get!_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
t.get! t.max! = t.max!
source
theorem Std.ExtTreeSet.getD_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} :
t.getD t.max! fallback = t.max!
source
theorem Std.ExtTreeSet.max!_erase_eq_of_not_compare_max!_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k t.max! = Ordering.eq) :
(t.erase k).max! = t.max!
source
theorem Std.ExtTreeSet.max!_erase_le_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) :
(cmp (t.erase k).max! t.max!).isLE = true
source
theorem Std.ExtTreeSet.max!_eq_getLast!_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] :
t.max! = t.toList.getLast!
source
theorem Std.ExtTreeSet.max?_eq_some_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.max? = some (t.maxD fallback)
source
theorem Std.ExtTreeSet.maxD_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {fallback : α} :
∅.maxD fallback = fallback
source
theorem Std.ExtTreeSet.max!_eq_maxD_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] :
t.max! = t.maxD default
source
theorem Std.ExtTreeSet.maxD_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {km fallback : α} :
t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.maxD_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (he : t ≠ ∅) {km fallback : α} :
t.maxD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true
source
theorem Std.ExtTreeSet.maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.maxD_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} :
(cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true
source
theorem Std.ExtTreeSet.self_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} :
(cmp k ((t.insert k).maxD fallback)).isLE = true
source
theorem Std.ExtTreeSet.contains_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.contains (t.maxD fallback) = true
source
theorem Std.ExtTreeSet.maxD_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.maxD fallback ∈ t
source
theorem Std.ExtTreeSet.le_maxD_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) {fallback : α} :
(cmp k (t.maxD fallback)).isLE = true
source
theorem Std.ExtTreeSet.le_maxD_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) {fallback : α} :
(cmp k (t.maxD fallback)).isLE = true
source
theorem Std.ExtTreeSet.maxD_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} :
(cmp (t.maxD fallback) k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true
source
theorem Std.ExtTreeSet.get?_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} :
t.get? (t.maxD fallback) = some (t.maxD fallback)
source
theorem Std.ExtTreeSet.get_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} {hc : t.maxD fallback ∈ t} :
t.get (t.maxD fallback) hc = t.maxD fallback
source
theorem Std.ExtTreeSet.get!_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} :
t.get! (t.maxD fallback) = t.maxD fallback
source
theorem Std.ExtTreeSet.getD_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback fallback' : α} :
t.getD (t.maxD fallback) fallback' = t.maxD fallback
source
theorem Std.ExtTreeSet.maxD_erase_eq_of_not_compare_maxD_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k (t.maxD fallback) = Ordering.eq) :
(t.erase k).maxD fallback = t.maxD fallback
source
theorem Std.ExtTreeSet.maxD_erase_le_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (he : t.erase k ≠ ∅) {fallback : α} :
(cmp ((t.erase k).maxD fallback) (t.maxD fallback)).isLE = true
source
theorem Std.ExtTreeSet.maxD_eq_getLastD_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} :
t.maxD fallback = t.toList.getLastD fallback
source
theorem Std.ExtTreeSet.ext_get? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} (h : ∀ (k : α), t₁.get? k = t₂.get? k) :
t₁ = t₂
source
theorem Std.ExtTreeSet.ext_get?_iff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} :
t₁ = t₂ ↔ ∀ (k : α), t₁.get? k = t₂.get? k
source
theorem Std.ExtTreeSet.ext_contains {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} (h : ∀ (k : α), t₁.contains k = t₂.contains k) :
t₁ = t₂
source
theorem Std.ExtTreeSet.ext_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} (h : ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) :
t₁ = t₂
source
theorem Std.ExtTreeSet.ext_mem_iff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} :
t₁ = t₂ ↔ ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂
source
theorem Std.ExtTreeSet.ext_toList {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : ExtTreeSet α cmp} [TransCmp cmp] (h : t₁.toList.Perm t₂.toList) :
t₁ = t₂
source
theorem Std.ExtTreeSet.toList_inj {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : ExtTreeSet α cmp} [TransCmp cmp] :
t₁.toList = t₂.toList ↔ t₁ = t₂
source
theorem Std.ExtTreeSet.toList_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} :
(filter f t).toList = List.filter f t.toList
source
theorem Std.ExtTreeSet.filter_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} :
filter f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = false
source
@[simp]
theorem Std.ExtTreeSet.mem_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} {k : α} :
k ∈ filter f t ↔ ∃ (h : k ∈ t), f (t.get k h) = true
source
theorem Std.ExtTreeSet.contains_of_contains_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} {k : α} :
(filter f t).contains k = true → t.contains k = true
source
theorem Std.ExtTreeSet.mem_of_mem_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} {k : α} :
k ∈ filter f t → k ∈ t
source
theorem Std.ExtTreeSet.size_filter_le_size {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} :
(filter f t).size ≤ t.size
source
theorem Std.ExtTreeSet.size_filter_eq_size_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} :
(filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
source
theorem Std.ExtTreeSet.filter_eq_self_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} :
filter f t = t ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
source
@[simp]
theorem Std.ExtTreeSet.get?_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} {k : α} :
(filter f t).get? k = Option.filter f (t.get? k)
source
@[simp]
theorem Std.ExtTreeSet.get_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} {k : α} {h : k ∈ filter f t} :
(filter f t).get k h = t.get k ⋯
source
theorem Std.ExtTreeSet.get!_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {f : α → Bool} {k : α} :
(filter f t).get! k = (Option.filter f (t.get? k)).get!
source
theorem Std.ExtTreeSet.getD_filter {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {f : α → Bool} {k fallback : α} :
(filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback