Ordset

📁 Source: Mathlib/Data/Ordmap/Ordset.lean

Statistics

Metric	Count
Definitions Valid, Valid', Ordset, instDecidablePred, erase, find, insert, insert', instEmptyCollection, instInhabited, instInsert, instMembership, instSingleton, map, mem, decidable, nil, singleton, size	19
Theorems bal, balance, balance', balance'_aux, balance'_lemma, balanceL, balanceL_aux, balanceR, balanceR_aux, dual, dual_iff, eraseMax_aux, eraseMin_aux, erase_aux, glue, glue_aux, left, map_aux, merge_aux, merge_aux₁, merge_lemma, mono_left, mono_right, node, node', node3L, node3R, node4L, node4L_lemma₁, node4L_lemma₂, node4L_lemma₃, node4L_lemma₄, node4L_lemma₅, of_gt, of_lt, ord, right, rotateL, rotateL_lemma₁, rotateL_lemma₂, rotateL_lemma₃, rotateL_lemma₄, rotateR, sz, trans_left, trans_right, valid, dual, dual_iff, left, merge, right, size_eq, valid, valid, valid, valid, insert'_eq_insertWith, valid, valid, valid_aux, insert_eq_insertWith, valid, size_erase_of_mem, valid'_nil, valid'_singleton, valid_nil, valid_singleton, empty_iff, pos_size_of_mem	70
Total	89

Ordnode

Definitions

Name	Category	Theorems
Valid 📖	MathDef	4 math, 1 bridge math: Valid.dual_iff, Valid'.valid, valid_nil, valid_singleton bridge: Ordset.empty_iff
Valid' 📖	CompData	3 math math: valid'_singleton, Valid'.dual_iff, valid'_nil

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
insert'_eq_insertWith 📖	mathematical	—	insert' Preorder.toLE insertWith	—	insert'.eq_def insertWith.eq_def
insert_eq_insertWith 📖	mathematical	—	insert Preorder.toLE insertWith	—	insert.eq_def insertWith.eq_def
size_erase_of_mem 📖	mathematical	Valid' Ordnode instMembership Preorder.toLE	size erase	—	Valid'.left Valid'.right erase.eq_def Valid'.erase_aux size_balanceR Valid'.bal Valid'.sz pos_size_of_mem add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Valid'.glue size_balanceL
valid'_nil 📖	mathematical	Bounded nil	Valid'	—	—
valid'_singleton 📖	mathematical	Bounded nil WithTop.some WithBot.some	Valid' Ordnode instSingleton	—	Valid'.node valid'_nil zero_le_one Nat.instZeroLEOneClass
valid_nil 📖	mathematical	—	Valid nil	—	valid'_nil
valid_singleton 📖	mathematical	—	Valid Ordnode instSingleton	—	valid'_singleton

Ordnode.Valid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual 📖	mathematical	Ordnode.Valid	OrderDual OrderDual.instPreorder Ordnode.dual	—	Ordnode.Valid'.dual
dual_iff 📖	mathematical	—	Ordnode.Valid OrderDual OrderDual.instPreorder Ordnode.dual	—	Ordnode.Valid'.dual_iff
left 📖	—	Ordnode.Valid Ordnode.node	—	—	Ordnode.Valid'.valid Ordnode.Valid'.left
merge 📖	mathematical	Ordnode.Valid Ordnode.All Preorder.toLT	Ordnode.merge	—	Ordnode.Valid'.merge_aux
right 📖	—	Ordnode.Valid Ordnode.node	—	—	Ordnode.Valid'.valid Ordnode.Valid'.right
size_eq 📖	mathematical	Ordnode.Valid Ordnode.node	Ordnode.size	—	Ordnode.Valid'.sz

Ordnode.Valid'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bal 📖	mathematical	Ordnode.Valid'	Ordnode.Balanced	—	—
balance 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Nat.dist Ordnode.size	Ordnode.balance	—	Ordnode.balance_eq_balance' bal sz balance'
balance' 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Nat.dist Ordnode.size	Ordnode.balance'	—	balance'_aux balance'_lemma Ordnode.BalancedSz.symm
balance'_aux 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.size	Ordnode.balance'	—	Ordnode.balance'.eq_1 node' rotateL rotateR not_lt
balance'_lemma 📖	—	Ordnode.BalancedSz Nat.dist Ordnode.size	—	—	le_trans Nat.dist_tri_right Nat.dist_tri_left' add_le_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Nat.dist_tri_right'
balanceL 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.Raised Ordnode.size Ordnode.BalancedSz	Ordnode.balanceL	—	Ordnode.balanceL_eq_balance' bal sz balance' Ordnode.Raised.dist_le' Ordnode.Raised.dist_le
balanceL_aux 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.size Ordnode.delta	Ordnode.balanceL	—	Ordnode.balanceL_eq_balance sz Ordnode.balance_eq_balance' bal balance'_aux le_trans
balanceR 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.Raised Ordnode.size Ordnode.BalancedSz	Ordnode.balanceR	—	dual_iff Ordnode.dual_balanceR balanceL dual Ordnode.balance_sz_dual
balanceR_aux 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.size Ordnode.delta	Ordnode.balanceR	—	dual_iff Ordnode.dual_balanceR balanceL_aux dual Ordnode.size_dual
dual 📖	mathematical	Ordnode.Valid'	OrderDual OrderDual.instPreorder Ordnode.dual	—	Ordnode.valid'_nil Ordnode.Bounded.dual ord add_comm Ordnode.size_dual Ordnode.BalancedSz.symm
dual_iff 📖	mathematical	—	Ordnode.Valid' OrderDual OrderDual.instPreorder Ordnode.dual	—	dual OrderDual.Preorder.dual_dual Ordnode.dual_dual
eraseMax_aux 📖	mathematical	Ordnode.Valid' Ordnode.node	Ordnode.eraseMax Ordnode.node' WithTop.some Ordnode.findMax' Ordnode.size	—	Ordnode.Sized.eq_node' sz left right balanceL bal Ordnode.eraseMax.eq_3 Ordnode.size_balanceL Ordnode.size_node
eraseMin_aux 📖	mathematical	Ordnode.Valid' Ordnode.node	WithBot.some Ordnode.findMin' Ordnode.eraseMin Ordnode.node' Ordnode.size	—	eraseMax_aux dual Ordnode.findMax'_dual dual_iff Ordnode.size_dual Ordnode.dual_eraseMin Ordnode.dual_node'
erase_aux 📖	mathematical	Ordnode.Valid'	Ordnode.erase Preorder.toLE Ordnode.Raised Ordnode.size	—	zero_add left right sz bal balanceR Ordnode.size_balanceR Ordnode.Raised.add_right glue balanceL Ordnode.size_balanceL Ordnode.Raised.add_left
glue 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Ordnode.size	Ordnode.glue	—	glue_aux trans_right ord trans_left Ordnode.Bounded.to_sep
glue_aux 📖	mathematical	Ordnode.Valid' Ordnode.All Preorder.toLT Ordnode.BalancedSz Ordnode.size	Ordnode.glue	—	zero_add Ordnode.splitMax_eq eraseMax_aux Ordnode.Sized.eq_node' sz balanceR of_gt Ordnode.findMax'_all Ordnode.Bounded.to_nil ord Ordnode.All.imp Ordnode.Bounded.mono_left le_of_lt Ordnode.size_balanceR bal add_right_comm Ordnode.splitMin_eq eraseMin_aux balanceL of_lt Ordnode.findMin'_all Ordnode.Bounded.mono_right Ordnode.all_iff_forall Ordnode.size_balanceL add_assoc
left 📖	mathematical	Ordnode.Valid' Ordnode.node	WithTop.some	—	ord sz bal
map_aux 📖	mathematical	StrictMono Ordnode.Valid'	Ordnode.map Ordnode.size	—	Ordnode.valid'_nil ord left right sz bal
merge_aux 📖	mathematical	Ordnode.Valid' Ordnode.All Preorder.toLT	Ordnode.merge Ordnode.size	—	zero_add Ordnode.merge_node of_lt Ordnode.Bounded.to_nil ord Ordnode.All.imp left merge_aux₁ right of_gt dual add_comm Ordnode.size_dual dual_iff Ordnode.dual_balanceR glue_aux not_lt
merge_aux₁ 📖	mathematical	Ordnode.Valid' Ordnode.node Ordnode.delta WithTop.some Ordnode.size	Ordnode.balanceL	—	bal Ordnode.delta.eq_1 sz add_right_comm balanceL_aux right merge_lemma Ordnode.balanceL_eq_balance Ordnode.balance_eq_balance' Ordnode.size_balance' Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.term_add_term Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat add_zero Mathlib.Tactic.Abel.const_add_term
merge_lemma 📖	—	—	—	—	—
mono_left 📖	—	Preorder.toLE Ordnode.Valid' WithBot.some	—	—	Ordnode.Bounded.mono_left ord sz bal
mono_right 📖	—	Preorder.toLE Ordnode.Valid' WithTop.some	—	—	Ordnode.Bounded.mono_right ord sz bal
node 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Ordnode.size	Ordnode.node	—	ord sz bal
node' 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Ordnode.size	Ordnode.node'	—	node
node3L 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Ordnode.size	Ordnode.node3L	—	node'
node3R 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.BalancedSz Ordnode.size	Ordnode.node3R	—	node'
node4L 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.size Ordnode.ratio Ordnode.delta	Ordnode.node4L	—	add_eq_zero Unique.instSubsingleton Nat.instCanonicallyOrderedAdd Ordnode.Sized.size_eq sz not_le_of_gt zero_add bal MulZeroClass.mul_zero le_trans mul_add Distrib.leftDistribClass mul_left_comm add_le_add_right IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instAtLeastTwoHAddOfNat two_mul add_lt_add_of_lt_of_le IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add one_mul mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono node4L_lemma₁ node4L_lemma₂ node4L_lemma₃ node4L_lemma₄ node4L_lemma₅ node' left right
node4L_lemma₁ 📖	—	—	—	—	—
node4L_lemma₂ 📖	—	—	—	—	—
node4L_lemma₃ 📖	—	—	—	—	—
node4L_lemma₄ 📖	—	—	—	—	—
node4L_lemma₅ 📖	—	—	—	—	—
of_gt 📖	—	Ordnode.Valid' Ordnode.Bounded Ordnode.nil WithBot.some Ordnode.All Preorder.toLT	—	—	Ordnode.Bounded.of_gt ord sz bal
of_lt 📖	—	Ordnode.Valid' Ordnode.Bounded Ordnode.nil WithTop.some Ordnode.All Preorder.toLT	—	—	Ordnode.Bounded.of_lt ord sz bal
ord 📖	mathematical	Ordnode.Valid'	Ordnode.Bounded	—	—
right 📖	mathematical	Ordnode.Valid' Ordnode.node	WithBot.some	—	ord sz bal
rotateL 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.size Ordnode.delta	Ordnode.rotateL	—	Ordnode.Sized.size_eq sz le_trans Ordnode.rotateL_node mul_lt_mul_iff_right₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE lt_of_le_of_lt bal le_antisymm Ordnode.balancedSz_zero Ordnode.BalancedSz.symm add_comm rotateL_lemma₁ rotateL_lemma₂ rotateL_lemma₃ node3L left right not_lt node4L zero_le_one Nat.instZeroLEOneClass rotateL_lemma₄
rotateL_lemma₁ 📖	—	—	—	—	—
rotateL_lemma₂ 📖	—	—	—	—	—
rotateL_lemma₃ 📖	—	—	—	—	—
rotateL_lemma₄ 📖	—	—	—	—	—
rotateR 📖	mathematical	Ordnode.Valid' WithTop.some WithBot.some Ordnode.size Ordnode.delta	Ordnode.rotateR	—	dual_iff Ordnode.dual_rotateR rotateL dual Ordnode.size_dual add_comm
sz 📖	mathematical	Ordnode.Valid'	Ordnode.Sized	—	—
trans_left 📖	—	Ordnode.Bounded WithTop.some Ordnode.Valid' WithBot.some	—	—	Ordnode.Bounded.trans_left ord sz bal
trans_right 📖	—	Ordnode.Valid' WithTop.some Ordnode.Bounded WithBot.some	—	—	Ordnode.Bounded.trans_right ord sz bal
valid 📖	mathematical	Ordnode.Valid'	Ordnode.Valid	—	Ordnode.Bounded.weak ord sz bal

Ordnode.erase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	Ordnode.Valid	Ordnode.erase Preorder.toLE	—	Ordnode.Valid'.erase_aux

Ordnode.eraseMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	Ordnode.Valid	Ordnode.eraseMax	—	Ordnode.Valid.dual_iff Ordnode.dual_eraseMax Ordnode.eraseMin.valid Ordnode.Valid.dual

Ordnode.eraseMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	Ordnode.Valid	Ordnode.eraseMin	—	Ordnode.valid_nil Ordnode.Sized.eq_node' Ordnode.Valid'.sz Ordnode.Valid'.valid Ordnode.Valid'.eraseMin_aux

Ordnode.insert

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	Ordnode.Valid	Ordnode.insert Preorder.toLE	—	Ordnode.insert_eq_insertWith Ordnode.insertWith.valid le_rfl

Ordnode.insert'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	Ordnode.Valid	Ordnode.insert' Preorder.toLE	—	Ordnode.insert'_eq_insertWith Ordnode.insertWith.valid

Ordnode.insertWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	Preorder.toLE Ordnode.Valid	Ordnode.insertWith	—	valid_aux
valid_aux 📖	mathematical	Preorder.toLE Ordnode.Valid' Ordnode.Bounded Ordnode.nil WithTop.some WithBot.some	Ordnode.insertWith Ordnode.Raised Ordnode.size	—	Ordnode.valid'_singleton eq_2 cmpLE.eq_1 Ordnode.Bounded.mono_right le_trans Ordnode.Bounded.mono_left Ordnode.Valid'.left lt_of_le_not_ge Ordnode.Valid'.bal Ordnode.Valid'.balanceL Ordnode.Valid'.right Ordnode.size_balanceL Ordnode.Valid'.sz Ordnode.Sized.size_eq Ordnode.Raised.add_right total_of Ordnode.Valid'.balanceR Ordnode.size_balanceR Ordnode.Raised.add_left

Ordnode.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valid 📖	mathematical	StrictMono Ordnode.Valid	Ordnode.map	—	Ordnode.Valid'.map_aux

Ordset

Definitions

Name	Category	Theorems
erase 📖	CompOp	—
find 📖	CompOp	—
insert 📖	CompOp	—
insert' 📖	CompOp	—
instEmptyCollection 📖	CompOp	1 bridge bridge: empty_iff
instInhabited 📖	CompOp	—
instInsert 📖	CompOp	—
instMembership 📖	CompOp	—
instSingleton 📖	CompOp	—
map 📖	CompOp	—
mem 📖	CompOp	—
nil 📖	CompOp	—
singleton 📖	CompOp	—
size 📖	CompOp	1 math math: pos_size_of_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty_iff 📖	bridging (iff)	—	Ordset instEmptyCollection Ordnode.empty Ordnode Ordnode.Valid	Ordnode.empty	—
pos_size_of_mem 📖	mathematical	Ordset instMembership	size	—	Ordnode.pos_size_of_mem Ordnode.Valid'.sz

Ordset.Empty

Definitions

Name	Category	Theorems
instDecidablePred 📖	CompOp	—

Ordset.mem

Definitions

Name	Category	Theorems
decidable 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Ordset 📖	CompOp	1 bridge bridge: Ordset.empty_iff

---

← Back to Index