theorem
rbmap.eq_some_of_to_value_eq_some
{α : Type u}
{β : Type v}
{e : option (α × β)}
{v : β} :
rbmap.to_value e = option.some v → (∃ (k : α), e = option.some (k, v))
theorem
rbmap.mem_of_mem_of_eqv
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{m : rbmap α β lt}
{k₁ k₂ : α} :
k₁ ∈ m → strict_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 = option.none → k ∉ 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 = option.none → k ∉ 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₁ = option.some e → k₁ ∈ 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 = option.some v → k ∈ 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 = option.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₁ = option.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₁ = option.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) :
theorem
rbmap.constains_correct
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
[decidable_rel lt]
[is_strict_weak_order α lt]
(k : α)
(m : rbmap α β lt) :
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 : β) :
theorem
rbmap.mem_insert
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
[decidable_rel lt]
[is_strict_weak_order α lt]
(k : α)
(m : rbmap α β lt)
(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 : β) :
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} :
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} :
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₂ = option.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 = option.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₂ = option.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 = option.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 : β) :
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 : β) :
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 : β) :
theorem
rbmap.mem_of_min_eq
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
[is_strict_total_order α lt]
{k : α}
{v : β}
{m : rbmap α β lt} :
m.min = option.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 = option.some (k, v) → k ∈ m
theorem
rbmap.min_is_minimal
{α : Type u}
{β : Type v}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{k : α}
{v : β}
{m : rbmap α β lt} :
m.min = option.some (k, v) → ∀ {k' : α}, k' ∈ m → strict_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 = option.some (k, v) → ∀ {k' : α}, k' ∈ m → strict_weak_order.equiv k k' ∨ lt k' k