Commit 2023-06-02 11:07 2afe8cb1

View on Github →

feat: port Data.Ordmap.Ordset (#4541)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Ordmap/Ordnode.lean

added theorem Ordnode.size_nil

added theorem Ordnode.size_node

Created Mathlib/Data/Ordmap/Ordset.lean

added theorem Ordnode.All.imp

added theorem Ordnode.Any.imp

added theorem Ordnode.Balanced.dual

added def Ordnode.Balanced

added theorem Ordnode.BalancedSz.symm

added def Ordnode.BalancedSz

added theorem Ordnode.Bounded.dual

added theorem Ordnode.Bounded.dual_iff

added theorem Ordnode.Bounded.mem_gt

added theorem Ordnode.Bounded.mem_lt

added theorem Ordnode.Bounded.mono_left

added theorem Ordnode.Bounded.mono_right

added theorem Ordnode.Bounded.of_gt

added theorem Ordnode.Bounded.of_lt

added theorem Ordnode.Bounded.to_lt

added theorem Ordnode.Bounded.to_nil

added theorem Ordnode.Bounded.to_sep

added theorem Ordnode.Bounded.trans_left

added theorem Ordnode.Bounded.trans_right

added theorem Ordnode.Bounded.weak

added theorem Ordnode.Bounded.weak_left

added theorem Ordnode.Bounded.weak_right

added def Ordnode.Bounded

added theorem Ordnode.Raised.add_left

added theorem Ordnode.Raised.add_right

added theorem Ordnode.Raised.dist_le'

added theorem Ordnode.Raised.dist_le

added theorem Ordnode.Raised.right

added def Ordnode.Raised

added theorem Ordnode.Sized.balance'

added theorem Ordnode.Sized.dual

added theorem Ordnode.Sized.dual_iff

added theorem Ordnode.Sized.eq_node'

added theorem Ordnode.Sized.induction

added theorem Ordnode.Sized.node'

added theorem Ordnode.Sized.node3L

added theorem Ordnode.Sized.node3R

added theorem Ordnode.Sized.node4L

added theorem Ordnode.Sized.pos

added theorem Ordnode.Sized.rotateL

added theorem Ordnode.Sized.rotateL_size

added theorem Ordnode.Sized.rotateR

added theorem Ordnode.Sized.rotateR_size

added theorem Ordnode.Sized.size_eq

added theorem Ordnode.Sized.size_eq_zero

added def Ordnode.Sized

added theorem Ordnode.Valid'.balance'

added theorem Ordnode.Valid'.balance'_aux

added theorem Ordnode.Valid'.balance'_lemma

added theorem Ordnode.Valid'.balance

added theorem Ordnode.Valid'.balanceL

added theorem Ordnode.Valid'.balanceL_aux

added theorem Ordnode.Valid'.balanceR

added theorem Ordnode.Valid'.balanceR_aux

added theorem Ordnode.Valid'.dual

added theorem Ordnode.Valid'.dual_iff

added theorem Ordnode.Valid'.eraseMax_aux

added theorem Ordnode.Valid'.eraseMin_aux

added theorem Ordnode.Valid'.erase_aux

added theorem Ordnode.Valid'.glue

added theorem Ordnode.Valid'.glue_aux

added theorem Ordnode.Valid'.left

added theorem Ordnode.Valid'.map_aux

added theorem Ordnode.Valid'.merge_aux

added theorem Ordnode.Valid'.merge_aux₁

added theorem Ordnode.Valid'.merge_lemma

added theorem Ordnode.Valid'.mono_left

added theorem Ordnode.Valid'.mono_right

added theorem Ordnode.Valid'.node'

added theorem Ordnode.Valid'.node3L

added theorem Ordnode.Valid'.node3R

added theorem Ordnode.Valid'.node4L

added theorem Ordnode.Valid'.node4L_lemma₁

added theorem Ordnode.Valid'.node4L_lemma₂

added theorem Ordnode.Valid'.node4L_lemma₃

added theorem Ordnode.Valid'.node4L_lemma₄

added theorem Ordnode.Valid'.node4L_lemma₅

added theorem Ordnode.Valid'.node

added theorem Ordnode.Valid'.of_gt

added theorem Ordnode.Valid'.of_lt

added theorem Ordnode.Valid'.right

added theorem Ordnode.Valid'.rotateL

added theorem Ordnode.Valid'.rotateL_lemma₁

added theorem Ordnode.Valid'.rotateL_lemma₂

added theorem Ordnode.Valid'.rotateL_lemma₃

added theorem Ordnode.Valid'.rotateL_lemma₄

added theorem Ordnode.Valid'.rotateR

added theorem Ordnode.Valid'.trans_left

added theorem Ordnode.Valid'.trans_right

added theorem Ordnode.Valid'.valid

added structure Ordnode.Valid'

added theorem Ordnode.Valid.dual

added theorem Ordnode.Valid.dual_iff

added theorem Ordnode.Valid.merge

added theorem Ordnode.Valid.size_eq

added def Ordnode.Valid

added theorem Ordnode.all_balance'

added theorem Ordnode.all_balanceL

added theorem Ordnode.all_balanceR

added theorem Ordnode.all_dual

added theorem Ordnode.all_iff_forall

added theorem Ordnode.all_node'

added theorem Ordnode.all_node3L

added theorem Ordnode.all_node3R

added theorem Ordnode.all_node4L

added theorem Ordnode.all_node4R

added theorem Ordnode.all_rotateL

added theorem Ordnode.all_rotateR

added theorem Ordnode.all_singleton

added theorem Ordnode.any_iff_exists

added theorem Ordnode.any_singleton

added def Ordnode.balance'

added def Ordnode.balanceL'

added theorem Ordnode.balanceL_eq_balance'

added theorem Ordnode.balanceL_eq_balance

added def Ordnode.balanceR'

added theorem Ordnode.balanceR_eq_balance'

added theorem Ordnode.balance_eq_balance'

added theorem Ordnode.balance_sz_dual

added theorem Ordnode.balancedSz_down

added theorem Ordnode.balancedSz_up

added theorem Ordnode.balancedSz_zero

added theorem Ordnode.delta_lt_false

added theorem Ordnode.dual_balance'

added theorem Ordnode.dual_balanceL

added theorem Ordnode.dual_balanceR

added theorem Ordnode.dual_dual

added theorem Ordnode.dual_eraseMax

added theorem Ordnode.dual_eraseMin

added theorem Ordnode.dual_insert

added theorem Ordnode.dual_node'

added theorem Ordnode.dual_node3L

added theorem Ordnode.dual_node3R

added theorem Ordnode.dual_node4L

added theorem Ordnode.dual_node4R

added theorem Ordnode.dual_rotateL

added theorem Ordnode.dual_rotateR

added theorem Ordnode.emem_iff_all

added theorem Ordnode.emem_iff_mem_toList

added theorem Ordnode.equiv_iff

added theorem Ordnode.erase.valid

added theorem Ordnode.eraseMax.valid

added theorem Ordnode.eraseMin.valid

added theorem Ordnode.findMax'_all

added theorem Ordnode.findMax'_dual

added theorem Ordnode.findMax_dual

added theorem Ordnode.findMin'_all

added theorem Ordnode.findMin'_dual

added theorem Ordnode.findMin_dual

added theorem Ordnode.foldr_cons_eq_toList

added theorem Ordnode.insert'.valid

added theorem Ordnode.insert'_eq_insertWith

added theorem Ordnode.insert.valid

added theorem Ordnode.insertWith.valid

added theorem Ordnode.insertWith.valid_aux

added theorem Ordnode.insert_eq_insertWith

added theorem Ordnode.length_toList'

added theorem Ordnode.length_toList

added theorem Ordnode.map.valid

added theorem Ordnode.merge_nil_left

added theorem Ordnode.merge_nil_right

added theorem Ordnode.merge_node

added def Ordnode.node3L

added theorem Ordnode.node3L_size

added def Ordnode.node3R

added theorem Ordnode.node3R_size

added def Ordnode.node4L

added theorem Ordnode.node4L_size

added def Ordnode.node4R

added theorem Ordnode.not_le_delta

added theorem Ordnode.pos_size_of_mem

added theorem Ordnode.raised_iff

added def Ordnode.realSize

added def Ordnode.rotateL

added theorem Ordnode.rotateL_nil

added theorem Ordnode.rotateL_node

added def Ordnode.rotateR

added theorem Ordnode.rotateR_nil

added theorem Ordnode.rotateR_node

added theorem Ordnode.size_balance'

added theorem Ordnode.size_balanceL

added theorem Ordnode.size_balanceR

added theorem Ordnode.size_dual

added theorem Ordnode.size_eq_realSize

added theorem Ordnode.size_erase_of_mem

added theorem Ordnode.splitMax_eq

added theorem Ordnode.splitMin_eq

added theorem Ordnode.toList_nil

added theorem Ordnode.toList_node

added theorem Ordnode.valid'_nil

added theorem Ordnode.valid'_singleton

added theorem Ordnode.valid_nil

added theorem Ordnode.valid_singleton

added def Ordset.Empty

added theorem Ordset.empty_iff

added def Ordset.erase

added def Ordset.find

added def Ordset.map

added def Ordset.mem

added theorem Ordset.pos_size_of_mem

added def Ordset.size

added def Ordset