Chain

📁 Source: Mathlib/Order/Preorder/Chain.lean

Statistics

Metric	Count
Definitions Chain, carrier, instBoundedOrderSubtypeMem, instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq, instOrderBotSubtypeMem, instOrderTopSubtypeMem, instPartialOrder, instSetLike, instUnique, map, ofIsMaxChain, IsChain, IsMaxChain, Chain, SuccChain, SuperChain	16
Theorems Chain', bot_mem, chain_le, chain_lt, coe_map, coe_mk, coe_ofIsMaxChain, ext, ext_iff, le_or_le, maxChain, max_chain', mem_coe_iff, mem_iff_forall_le_or_ge, mk_coe, symm_map, top_mem, diff, directed, directedOn, empty, exists3, image, image_embedding, image_embedding_iff, image_iso, image_iso_iff, image_relEmbedding, image_relEmbedding_iff, image_relIso, image_relIso_iff, insert, le_of_not_gt, lt_of_le, lt_of_not_ge, mono, mono_rel, not_le, not_lt, pair, preimage, preimage_embedding, preimage_iso, preimage_iso_iff, preimage_relEmbedding, preimage_relIso, singleton, succ, superChain_succChain, total, bot_mem, image, isChain, isEmpty_iff, nonempty_iff, not_superChain, top_mem, isChain_image, isChain_range, isChain, isChain_coe_univ_iff, isChain_of_trichotomous, isChain_preimage_subtypeVal, isChain_union, isChain_univ_iff, subset_succChain, succChain_spec	67
Total	83

Cycle

Definitions

Name	Category	Theorems
Chain 📖	MathDef	11 math math: Chain.nil, chain_range_succ, Function.periodicOrbit_chain, Function.periodicOrbit_chain', chain_of_pairwise, chain_iff_pairwise, chain_singleton, chain_map, chain_mono, chain_coe_cons, chain_ne_nil

Flag

Definitions

Name	Category	Theorems
carrier 📖	CompOp	1 math math: Chain'
instBoundedOrderSubtypeMem 📖	CompOp	—
instLinearOrderSubtypeMemOfDecidableLEOfDecidableLTOfDecidableEq 📖	CompOp	—
instOrderBotSubtypeMem 📖	CompOp	—
instOrderTopSubtypeMem 📖	CompOp	—
instPartialOrder 📖	CompOp	—
instSetLike 📖	CompOp	25 math math: coe_ofIsMaxChain, isMax_coe, coe_map, bot_mem, top_mem, IsChain.exists_subset_flag, coe_covBy_coe, chain_le, exists_mem_mem, isMin_coe, exists_mem, grade_coe, mem_rangeFin, coe_mk, chain_lt, mem_iff_forall_le_or_ge, mk_coe, Module.Basis.mem_toFlag, ext_iff, Module.Basis.toFlag_carrier, mem_coe_iff, rangeFin_carrier, coe_wcovBy_coe, coe_smul, maxChain
instUnique 📖	CompOp	—
map 📖	CompOp	2 math math: coe_map, symm_map
ofIsMaxChain 📖	CompOp	1 math math: coe_ofIsMaxChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Chain' 📖	mathematical	—	IsChain carrier	—	—
bot_mem 📖	mathematical	—	Flag SetLike.instMembership instSetLike Bot.bot OrderBot.toBot	—	IsMaxChain.bot_mem maxChain
chain_le 📖	mathematical	—	IsChain SetLike.coe Flag instSetLike	—	Chain'
chain_lt 📖	mathematical	—	IsChain Preorder.toLT PartialOrder.toPreorder SetLike.coe Flag Preorder.toLE instSetLike	—	IsChain.lt_of_le chain_le
coe_map 📖	mathematical	—	SetLike.coe Flag Preorder.toLE instSetLike DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike map Set.image OrderIso instFunLikeOrderIso	—	—
coe_mk 📖	mathematical	IsChain	SetLike.coe Flag instSetLike	—	—
coe_ofIsMaxChain 📖	mathematical	IsMaxChain	SetLike.coe Flag instSetLike ofIsMaxChain	—	—
ext 📖	—	SetLike.coe Flag instSetLike	—	—	SetLike.ext'
ext_iff 📖	mathematical	—	SetLike.coe Flag instSetLike	—	ext
le_or_le 📖	—	Flag Preorder.toLE SetLike.instMembership instSetLike	—	—	IsChain.total instReflLe chain_le
maxChain 📖	mathematical	—	IsMaxChain SetLike.coe Flag instSetLike	—	chain_le max_chain'
max_chain' 📖	—	IsChain Set Set.instHasSubset carrier	—	—	—
mem_coe_iff 📖	mathematical	—	Set Set.instMembership SetLike.coe Flag instSetLike SetLike.instMembership	—	—
mem_iff_forall_le_or_ge 📖	mathematical	—	Flag Preorder.toLE SetLike.instMembership instSetLike	—	le_or_le of_not_not Set.ne_insert_of_notMem maxChain IsChain.insert chain_le Set.subset_insert
mk_coe 📖	mathematical	—	SetLike.coe Flag instSetLike Chain' max_chain'	—	ext Chain' max_chain'
symm_map 📖	mathematical	—	Equiv.symm Flag Preorder.toLE map OrderIso.symm	—	—
top_mem 📖	mathematical	—	Flag SetLike.instMembership instSetLike Top.top OrderTop.toTop	—	IsMaxChain.top_mem maxChain

IsChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diff 📖	mathematical	IsChain	Set Set.instSDiff	—	mono Set.diff_subset
directed 📖	mathematical	IsChain Order.Preimage	Directed Set Set.instMembership	—	by_cases refl
directedOn 📖	mathematical	IsChain	DirectedOn	—	total refl
empty 📖	mathematical	—	IsChain Set Set.instEmptyCollection	—	Set.pairwise_empty
exists3 📖	—	IsChain Set Set.instMembership	—	—	directedOn_iff_directed directed trans
image 📖	mathematical	IsChain	Set.image	—	—
image_embedding 📖	mathematical	IsChain	Set.image DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	image_relEmbedding
image_embedding_iff 📖	mathematical	—	IsChain Set.image DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	image_relEmbedding_iff
image_iso 📖	mathematical	IsChain	Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	image_relEmbedding
image_iso_iff 📖	mathematical	—	IsChain Set.image DFunLike.coe OrderIso instFunLikeOrderIso	—	image_relEmbedding_iff
image_relEmbedding 📖	mathematical	IsChain	Set.image DFunLike.coe RelEmbedding RelEmbedding.instFunLike	—	Set.mem_image
image_relEmbedding_iff 📖	mathematical	—	IsChain Set.image DFunLike.coe RelEmbedding RelEmbedding.instFunLike	—	Function.Injective.preimage_image RelEmbedding.injective preimage_relEmbedding image_relEmbedding
image_relIso 📖	mathematical	IsChain	Set.image DFunLike.coe RelIso RelIso.instFunLike	—	image_relEmbedding
image_relIso_iff 📖	mathematical	—	IsChain Set.image DFunLike.coe RelIso RelIso.instFunLike	—	image_relEmbedding_iff
insert 📖	mathematical	IsChain	Set Set.instInsert	—	Set.Pairwise.insert_of_symmetric
le_of_not_gt 📖	—	IsChain Preorder.toLE Set Set.instMembership Preorder.toLT	—	—	total instReflLe
lt_of_le 📖	mathematical	IsChain Preorder.toLE PartialOrder.toPreorder	Preorder.toLT	—	Ne.lt_of_le Ne.lt_of_le'
lt_of_not_ge 📖	mathematical	IsChain Preorder.toLE Set Set.instMembership	Preorder.toLT	—	total instReflLe lt_of_le_not_ge
mono 📖	—	Set Set.instHasSubset IsChain	—	—	Set.Pairwise.mono
mono_rel 📖	—	IsChain	—	—	Set.Pairwise.mono'
not_le 📖	mathematical	IsChain Preorder.toLE Set Set.instMembership	Preorder.toLT	—	lt_of_not_ge LE.le.not_gt
not_lt 📖	mathematical	IsChain Preorder.toLE Set Set.instMembership	Preorder.toLT	—	le_of_not_gt LT.lt.not_ge
pair 📖	mathematical	—	IsChain Set Set.instInsert Set.instSingletonSet	—	insert singleton Set.eq_of_mem_singleton
preimage 📖	mathematical	IsChain	Set.preimage	—	—
preimage_embedding 📖	mathematical	IsChain	Set.preimage DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding	—	preimage_relEmbedding
preimage_iso 📖	mathematical	IsChain	Set.preimage DFunLike.coe OrderIso instFunLikeOrderIso	—	preimage_relEmbedding
preimage_iso_iff 📖	mathematical	—	IsChain Set.preimage DFunLike.coe OrderIso instFunLikeOrderIso	—	OrderIso.image_preimage image_iso preimage_iso
preimage_relEmbedding 📖	mathematical	IsChain	Set.preimage DFunLike.coe RelEmbedding RelEmbedding.instFunLike	—	RelEmbedding.injective
preimage_relIso 📖	mathematical	IsChain	Set.preimage DFunLike.coe RelIso RelIso.instFunLike	—	preimage_relEmbedding
singleton 📖	mathematical	—	IsChain Set Set.instSingletonSet	—	Set.pairwise_singleton
succ 📖	mathematical	IsChain	SuccChain	—	succChain_spec
superChain_succChain 📖	mathematical	IsChain IsMaxChain	SuperChain SuccChain	—	succChain_spec ssubset_iff_subset_ne Set.instIsNonstrictStrictOrderSubsetSSubset Set.instAntisymmSubset
total 📖	—	IsChain Set Set.instMembership	—	—	eq_or_ne refl

IsMaxChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem 📖	mathematical	IsMaxChain	Set Set.instMembership Bot.bot OrderBot.toBot	—	Set.mem_insert IsChain.insert bot_le Set.subset_insert
image 📖	mathematical	IsMaxChain	Set.image DFunLike.coe RelIso RelIso.instFunLike	—	IsChain.image RelIso.map_rel_iff isChain RelIso.coe_fn_toEquiv Equiv.eq_preimage_iff_image_eq Equiv.image_symm_eq_preimage Equiv.subset_symm_image
isChain 📖	mathematical	IsMaxChain	IsChain	—	—
isEmpty_iff 📖	mathematical	IsMaxChain	IsEmpty Set Set.instEmptyCollection	—	Set.eq_empty_of_isEmpty instIsEmptySubtype Set.singleton_ne_empty IsChain.singleton
nonempty_iff 📖	mathematical	IsMaxChain	Set.Nonempty	—	not_iff_not isEmpty_iff
not_superChain 📖	mathematical	IsMaxChain	SuperChain	—	HasSSubset.SSubset.ne Set.instIrreflSSubset
top_mem 📖	mathematical	IsMaxChain	Set Set.instMembership Top.top OrderTop.toTop	—	Set.mem_insert IsChain.insert le_top Set.subset_insert

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isChain_image 📖	mathematical	Monotone IsChain Preorder.toLE	Set.image	—	IsChain.image
isChain_range 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsChain Preorder.toLE Set.range	—	Set.image_univ isChain_image isChain_of_trichotomous instTrichotomousLe

OmegaCompletePartialOrder

Definitions

Name	Category	Theorems
Chain 📖	CompOp	21 math math: le_ωSup, Part.Fix.approx_mem_approxChain, Chain.zip_coe, ωSup_le_iff, Chain.pair_zero, Chain.map_le_map, Chain.range_pair, ContinuousHom.forall_forall_merge, Chain.directed, Part.mem_ωSup, Chain.ext_iff, Chain.instOrderHomClassNat, Part.mem_chain_of_mem_ωSup, ωScottContinuous.isLUB, Scott.isωSup_iff_isLUB, Chain.map_coe, ContinuousHom.forall_forall_merge', Chain.isChain_range, Chain.mem_map_iff, Chain.pair_succ, isLUB_range_ωSup

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isChain 📖	mathematical	Set.Subsingleton	IsChain	—	pairwise

(root)

Definitions

Name	Category	Theorems
IsChain 📖	MathDef	32 math math: IsChain.preimage_iso_iff, IsChain.pair, IsChain.image_embedding_iff, isChain_coe_univ_iff, isChain_union, ChainClosure.isChain, ChainCompletePartialOrder.IsExtremePt.bot_isChain, IsChain.image_relEmbedding_iff, isChain_and_isAntichain_iff_subsingleton, Flag.Chain', IsChain.singleton, Flag.chain_le, IsChain.image_relIso_iff, Set.Subsingleton.isChain, Set.exists_eq_chainHeight_of_chainHeight_ne_top, Monotone.isChain_range, IsMaxChain.isChain, isChain_preimage_subtypeVal, SimpleGraph.isClique_iff_isChain_adj, IsChain.empty, Set.not_isChain_of_chainHeight_lt_encard, Flag.chain_lt, isChain_univ_iff, IsChain.image_iso_iff, Set.exists_isChain_of_le_chainHeight, OmegaCompletePartialOrder.Chain.isChain_range, Set.chainHeight_eq_iSup, Set.exists_eq_chainHeight_of_finite, Module.Basis.isChain_range_flag, isChain_of_trichotomous, NonemptyChain.isChain', Set.chainHeight_eq_top_iff
IsMaxChain 📖	MathDef	5 math math: maxChain_spec, Module.Basis.isMaxChain_range_flag, IsMaxChain.range_fin_of_covBy, IsChain.exists_maxChain, Flag.maxChain
SuccChain 📖	CompOp	5 math math: succChain_spec, IsChain.succ, subset_succChain, IsChain.superChain_succChain, ChainClosure.succ_fixpoint_iff
SuperChain 📖	MathDef	2 math math: IsMaxChain.not_superChain, IsChain.superChain_succChain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isChain_coe_univ_iff 📖	mathematical	—	IsChain Set.Elem Set Set.instMembership Set.univ	—	Set.inter_univ isChain_preimage_subtypeVal
isChain_of_trichotomous 📖	mathematical	—	IsChain	—	trichotomous_of
isChain_preimage_subtypeVal 📖	mathematical	—	IsChain Set.Elem Set Set.instMembership Set.preimage Set.instInter	—	—
isChain_union 📖	mathematical	—	IsChain Set Set.instUnion	—	IsChain.eq_1 Set.pairwise_union_of_symmetric
isChain_univ_iff 📖	mathematical	—	IsChain Set.univ	—	isChain_of_trichotomous
subset_succChain 📖	mathematical	—	Set Set.instHasSubset SuccChain	—	succChain_spec Set.instReflSubset
succChain_spec 📖	mathematical	IsChain SuperChain	SuccChain	—	—

---

← Back to Index