mathlib documentation

data.rbmap.default

theorem rbmap.eq_some_of_to_value_eq_some {α : Type u} {β : Type v} {e : option × β)} {v : β} :
rbmap.to_value e = some v(∃ (k : α), e = some (k, v))
theorem rbmap.eq_none_of_to_value_eq_none {α : Type u} {β : Type v} {e : option × β)} :
theorem rbmap.not_mem_mk_rbmap {α : Type u} {β : Type v} {lt : α → α → Prop} (k : α) :
k mk_rbmap α β lt
theorem rbmap.not_mem_of_empty {α : Type u} {β : Type v} {lt : α → α → Prop} {m : rbmap α β lt} (k : α) :
m.empty = ttk m
theorem rbmap.mem_of_mem_of_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_weak_order α lt] {m : rbmap α β lt} {k₁ k₂ : α} :
k₁ mstrict_weak_order.equiv k₁ k₂k₂ m
theorem rbmap.not_mem_of_find_entry_none {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k : α} {m : rbmap α β lt} :
m.find_entry k = nonek m
theorem rbmap.not_mem_of_find_none {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k : α} {m : rbmap α β lt} :
m.find k = nonek m
theorem rbmap.mem_of_find_entry_some {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ : α} {e : α × β} {m : rbmap α β lt} :
m.find_entry k₁ = some ek₁ m
theorem rbmap.mem_of_find_some {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.find k = some vk m
theorem rbmap.find_entry_eq_find_entry_of_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {m : rbmap α β lt} {k₁ k₂ : α} :
strict_weak_order.equiv k₁ k₂m.find_entry k₁ = m.find_entry k₂
theorem rbmap.find_eq_find_of_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) :
strict_weak_order.equiv k₁ k₂m.find k₁ = m.find k₂
theorem rbmap.find_entry_correct {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (k : α) (m : rbmap α β lt) :
k m ∃ (e : α × β), m.find_entry k = some e strict_weak_order.equiv k e.fst
theorem rbmap.eqv_of_find_entry_some {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} {v : β} {m : rbmap α β lt} :
m.find_entry k₁ = some (k₂, v)strict_weak_order.equiv k₁ k₂
theorem rbmap.eq_of_find_entry_some {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {k₁ k₂ : α} {v : β} {m : rbmap α β lt} :
m.find_entry k₁ = some (k₂, v)k₁ = k₂
theorem rbmap.find_correct {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (k : α) (m : rbmap α β lt) :
k m ∃ (v : β), m.find k = some v
theorem rbmap.constains_correct {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (k : α) (m : rbmap α β lt) :
k m m.contains k = tt
theorem rbmap.mem_insert_of_incomp {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
¬lt k₁ k₂ ¬lt k₂ k₁k₁ m.insert k₂ v
theorem rbmap.mem_insert {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (k : α) (m : rbmap α β lt) (v : β) :
k m.insert k v
theorem rbmap.mem_insert_of_equiv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
strict_weak_order.equiv k₁ k₂k₁ m.insert k₂ v
theorem rbmap.mem_insert_of_mem {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ : α} {m : rbmap α β lt} (k₂ : α) (v : β) :
k₁ mk₁ m.insert k₂ v
theorem rbmap.equiv_or_mem_of_mem_insert {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} {v : β} {m : rbmap α β lt} :
k₁ m.insert k₂ vstrict_weak_order.equiv k₁ k₂ k₁ m
theorem rbmap.incomp_or_mem_of_mem_ins {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} {v : β} {m : rbmap α β lt} :
k₁ m.insert k₂ v¬lt k₁ k₂ ¬lt k₂ k₁ k₁ m
theorem rbmap.eq_or_mem_of_mem_ins {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {k₁ k₂ : α} {v : β} {m : rbmap α β lt} :
k₁ m.insert k₂ vk₁ = k₂ k₁ m
theorem rbmap.find_entry_insert_of_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (m : rbmap α β lt) {k₁ k₂ : α} (v : β) :
strict_weak_order.equiv k₁ k₂(m.insert k₁ v).find_entry k₂ = some (k₁, v)
theorem rbmap.find_entry_insert {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (m : rbmap α β lt) (k : α) (v : β) :
(m.insert k v).find_entry k = some (k, v)
theorem rbmap.find_insert_of_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (m : rbmap α β lt) {k₁ k₂ : α} (v : β) :
strict_weak_order.equiv k₁ k₂(m.insert k₁ v).find k₂ = some v
theorem rbmap.find_insert {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (m : rbmap α β lt) (k : α) (v : β) :
(m.insert k v).find k = some v
theorem rbmap.find_entry_insert_of_disj {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
lt k₁ k₂ lt k₂ k₁(m.insert k₁ v).find_entry k₂ = m.find_entry k₂
theorem rbmap.find_entry_insert_of_not_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
¬strict_weak_order.equiv k₁ k₂(m.insert k₁ v).find_entry k₂ = m.find_entry k₂
theorem rbmap.find_entry_insert_of_ne {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
k₁ k₂(m.insert k₁ v).find_entry k₂ = m.find_entry k₂
theorem rbmap.find_insert_of_disj {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
lt k₁ k₂ lt k₂ k₁(m.insert k₁ v).find k₂ = m.find k₂
theorem rbmap.find_insert_of_not_eqv {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
¬strict_weak_order.equiv k₁ k₂(m.insert k₁ v).find k₂ = m.find k₂
theorem rbmap.find_insert_of_ne {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {k₁ k₂ : α} (m : rbmap α β lt) (v : β) :
k₁ k₂(m.insert k₁ v).find k₂ = m.find k₂
theorem rbmap.mem_of_min_eq {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_total_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.min = some (k, v)k m
theorem rbmap.mem_of_max_eq {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_total_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.max = some (k, v)k m
theorem rbmap.eq_leaf_of_min_eq_none {α : Type u} {β : Type v} {lt : α → α → Prop} {m : rbmap α β lt} :
m.min = nonem = mk_rbmap α β lt
theorem rbmap.eq_leaf_of_max_eq_none {α : Type u} {β : Type v} {lt : α → α → Prop} {m : rbmap α β lt} :
m.max = nonem = mk_rbmap α β lt
theorem rbmap.min_is_minimal {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_weak_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.min = some (k, v)∀ {k' : α}, k' mstrict_weak_order.equiv k k' lt k k'
theorem rbmap.max_is_maximal {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_weak_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.max = some (k, v)∀ {k' : α}, k' mstrict_weak_order.equiv k k' lt k' k
theorem rbmap.min_is_minimal_of_total {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_total_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.min = some (k, v)∀ {k' : α}, k' mk = k' lt k k'
theorem rbmap.max_is_maximal_of_total {α : Type u} {β : Type v} {lt : α → α → Prop} [is_strict_total_order α lt] {k : α} {v : β} {m : rbmap α β lt} :
m.max = some (k, v)∀ {k' : α}, k' mk = k' lt k' k