mathlib3 documentation

data.rbmap.default

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.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 : α) :
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} :
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} :
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} :
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₂ : α} :
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) :
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} :
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) :
k m (v : β), m.find k = option.some v
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 : β) :
¬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₁ m k₁ 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₂ v strict_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₂ v k₁ = 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₂ = 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 : β) :
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 = 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.eq_leaf_of_min_eq_none {α : Type u} {β : Type v} {lt : α α Prop} {m : rbmap α β lt} :
m.min = option.none m = mk_rbmap α β lt
theorem rbmap.eq_leaf_of_max_eq_none {α : Type u} {β : Type v} {lt : α α Prop} {m : rbmap α β lt} :
m.max = option.none m = 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 = 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
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 = option.some (k, v) {k' : α}, k' m k = 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 = option.some (k, v) {k' : α}, k' m k = k' lt k' k