Basic

📁 Source: Mathlib/Order/Partition/Basic.lean

Statistics

Metric	Count
Definitions copy, instPartialOrder, instSetLike, parts, partscopyEquiv, removeBot	6
Theorems bot_lt_of_mem, bot_notMem, bot_notMem', coe_copy, coe_parts, coe_removeBot, disjoint, ext, ext_iff, iSup_eq, le_of_mem, mem_copy_iff, ne_bot_of_mem, pairwiseDisjoint, parts_nonempty, partscopyEquiv_apply_coe, partscopyEquiv_symm_apply_coe, sSupIndep, sSupIndep', sSup_eq, sSup_eq'	21
Total	27

Partition

Definitions

Name	Category	Theorems
copy 📖	CompOp	4 math math: coe_copy, partscopyEquiv_symm_apply_coe, mem_copy_iff, partscopyEquiv_apply_coe
instPartialOrder 📖	CompOp	—
instSetLike 📖	CompOp	13 math math: bot_notMem, pairwiseDisjoint, coe_copy, partscopyEquiv_symm_apply_coe, iSup_eq, ext_iff, sSupIndep, mem_copy_iff, sSup_eq, coe_removeBot, partscopyEquiv_apply_coe, parts_nonempty, coe_parts
parts 📖	CompOp	4 math math: sSupIndep', sSup_eq', bot_notMem', coe_parts
partscopyEquiv 📖	CompOp	2 math math: partscopyEquiv_symm_apply_coe, partscopyEquiv_apply_coe
removeBot 📖	CompOp	1 math math: coe_removeBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt_of_mem 📖	mathematical	Partition SetLike.instMembership instSetLike	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_lt_iff_ne_bot ne_bot_of_mem
bot_notMem 📖	mathematical	—	Partition SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_notMem'
bot_notMem' 📖	mathematical	—	Set Set.instMembership parts Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
coe_copy 📖	mathematical	—	SetLike.coe Partition instSetLike copy	—	—
coe_parts 📖	mathematical	—	parts SetLike.coe Partition instSetLike	—	—
coe_removeBot 📖	mathematical	sSupIndep SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	SetLike.coe Partition instSetLike removeBot Set Set.instSDiff Set.instSingletonSet Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
disjoint 📖	mathematical	Partition SetLike.instMembership instSetLike	Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder	—	sSupIndep.pairwiseDisjoint sSupIndep
ext 📖	—	Partition SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Partition SetLike.instMembership instSetLike	—	ext
iSup_eq 📖	mathematical	—	iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Partition SetLike.instMembership instSetLike	—	sSup_eq sSup_eq_iSup
le_of_mem 📖	mathematical	Partition SetLike.instMembership instSetLike	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	LE.le.trans_eq le_sSup sSup_eq
mem_copy_iff 📖	mathematical	—	Partition SetLike.instMembership instSetLike copy	—	—
ne_bot_of_mem 📖	—	Partition SetLike.instMembership instSetLike	—	—	bot_notMem
pairwiseDisjoint 📖	mathematical	—	Set.PairwiseDisjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder SetLike.coe Partition instSetLike	—	sSupIndep.pairwiseDisjoint sSupIndep'
parts_nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe Partition instSetLike	—	Set.nonempty_iff_ne_empty sSup_eq sSup_empty
partscopyEquiv_apply_coe 📖	mathematical	—	DFunLike.coe Equiv Partition SetLike.instMembership instSetLike copy EquivLike.toFunLike Equiv.instEquivLike partscopyEquiv Set Set.instMembership SetLike.coe	—	—
partscopyEquiv_symm_apply_coe 📖	mathematical	—	DFunLike.coe Equiv Partition SetLike.instMembership instSetLike copy EquivLike.toFunLike Equiv.instEquivLike Equiv.symm partscopyEquiv Set Set.instMembership SetLike.coe	—	—
sSupIndep 📖	mathematical	—	sSupIndep SetLike.coe Partition instSetLike	—	sSupIndep'
sSupIndep' 📖	mathematical	—	sSupIndep parts	—	—
sSup_eq 📖	mathematical	—	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice SetLike.coe Partition instSetLike	—	sSup_eq'
sSup_eq' 📖	mathematical	—	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice parts	—	—

---

← Back to Index