Basic

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

Statistics

Metric	Count
Definitions copy, instOrderTop, instPartialOrder, instSetLike, instUniqueBot, parts, partscopyEquiv, removeBot	8
Theorems bot_lt_of_mem, bot_notMem, bot_notMem', coe_copy, coe_parts, coe_removeBot, disjoint, eq_of_not_disjoint, eq_or_disjoint, existsUnique_of_mem_le, exists_le_of_mem_le, ext, ext_iff, iSup_eq, le_def, le_of_mem, mem_copy_iff, mem_removeBot, mem_top_iff, ne_bot_of_mem, ne_bot_of_mem', notMem_of_bot, pairwiseDisjoint, parts_nonempty, parts_top, parts_top_subset, partscopyEquiv_apply_coe, partscopyEquiv_symm_apply_coe, sSupIndep, sSupIndep', sSup_eq, sSup_eq', top_def	33
Total	41

Partition

Definitions

Name	Category	Theorems
copy 📖	CompOp	4 math math: coe_copy, partscopyEquiv_symm_apply_coe, mem_copy_iff, partscopyEquiv_apply_coe
instOrderTop 📖	CompOp	4 math math: parts_top, mem_top_iff, top_def, parts_top_subset
instPartialOrder 📖	CompOp	5 math math: parts_top, mem_top_iff, top_def, le_def, parts_top_subset
instSetLike 📖	CompOp	21 math math: existsUnique_of_mem_le, bot_notMem, parts_top, pairwiseDisjoint, exists_le_of_mem_le, coe_copy, mem_top_iff, partscopyEquiv_symm_apply_coe, le_def, iSup_eq, ext_iff, sSupIndep, mem_removeBot, mem_copy_iff, notMem_of_bot, sSup_eq, coe_removeBot, partscopyEquiv_apply_coe, parts_nonempty, coe_parts, parts_top_subset
instUniqueBot 📖	CompOp	—
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	3 math math: top_def, mem_removeBot, 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
eq_of_not_disjoint 📖	—	Partition SetLike.instMembership instSetLike Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder	—	—	eq_or_disjoint
eq_or_disjoint 📖	mathematical	Partition SetLike.instMembership instSetLike	Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder	—	disjoint
existsUnique_of_mem_le 📖	mathematical	Partition Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	ExistsUnique Partition SetLike.instMembership instSetLike Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	eq_of_not_disjoint ne_bot_of_mem Mathlib.Tactic.Contrapose.contrapose₄ le_bot_iff
exists_le_of_mem_le 📖	mathematical	Partition Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike	Partition SetLike.instMembership instSetLike Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	—
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_def 📖	mathematical	—	Partition Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	—
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	—	—
mem_removeBot 📖	mathematical	sSupIndep SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	Partition SetLike.instMembership instSetLike removeBot Set Set.instMembership	—	—
mem_top_iff 📖	mathematical	—	Partition SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	sSupIndep_singleton sSup_singleton top_def mem_removeBot Set.mem_singleton_iff
ne_bot_of_mem 📖	—	Partition SetLike.instMembership instSetLike	—	—	bot_notMem
ne_bot_of_mem' 📖	—	Partition SetLike.instMembership instSetLike	—	—	notMem_of_bot
notMem_of_bot 📖	mathematical	—	Partition Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder SetLike.instMembership instSetLike	—	bot_notMem le_bot_iff le_of_mem
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
parts_top 📖	mathematical	—	SetLike.coe Partition instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop Set Set.instSingletonSet	—	—
parts_top_subset 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Partition instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop Set.instSingletonSet	—	—
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	—	—
top_def 📖	mathematical	—	Top.top Partition OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop removeBot Set Set.instSingletonSet sSupIndep_singleton sSup_singleton CompleteLattice.toCompleteSemilatticeSup	—	—

---

← Back to Index