BourbakiWitt

📁 Source: Mathlib/Order/BourbakiWitt.lean

Statistics

Metric	Count
Definitions ChainCompletePartialOrder, IsAdmissible, IsExtremePt, bot, cSup, instOfCompleteLattice, instOmegaCompletePartialOrder, toPartialOrder, NonemptyChain, carrier, instPartialOrderNonemptyChain, instSetLikeNonemptyChain	12
Theorems base_isLeast, cSup_mem, image_self_subset_self, bot_eq_of_le_or_map_le, bot_isChain, map_le_of_mem_of_lt, mem_bot, mem_bot_iff_isExtremePt, setOf_isExtremePt_eq_bot, setOf_isExtremePt_isAdmissible, bot_isAdmissible, cSup_le, ici_isAdmissible, le_cSup, map_mem_bot, nonempty_fixedPoints_of_inflationary, subset_bot_iff, Nonempty', ext, ext_iff, isChain'	21
Total	33

ChainCompletePartialOrder

Definitions

Name	Category	Theorems
IsAdmissible 📖	CompData	3 math math: IsExtremePt.setOf_isExtremePt_isAdmissible, bot_isAdmissible, ici_isAdmissible
IsExtremePt 📖	CompData	3 math math: IsExtremePt.setOf_isExtremePt_isAdmissible, IsExtremePt.setOf_isExtremePt_eq_bot, IsExtremePt.mem_bot_iff_isExtremePt
bot 📖	CompOp	7 math math: IsExtremePt.bot_eq_of_le_or_map_le, subset_bot_iff, IsExtremePt.bot_isChain, bot_isAdmissible, IsExtremePt.mem_bot, IsExtremePt.setOf_isExtremePt_eq_bot, IsExtremePt.mem_bot_iff_isExtremePt
cSup 📖	CompOp	3 math math: le_cSup, cSup_le, IsAdmissible.cSup_mem
instOfCompleteLattice 📖	CompOp	—
instOmegaCompletePartialOrder 📖	CompOp	—
toPartialOrder 📖	CompOp	1 math math: IsAdmissible.base_isLeast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_isAdmissible 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder	IsAdmissible bot	—	IsAdmissible.base_isLeast ici_isAdmissible IsAdmissible.image_self_subset_self Set.mem_sInter IsAdmissible.cSup_mem subset_trans Set.instIsTransSubset Set.sInter_subset_of_mem
cSup_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder	cSup	—	—
ici_isAdmissible 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder	IsAdmissible Set.Ici	—	le_refl le_trans NonemptyChain.Nonempty' le_cSup
le_cSup 📖	mathematical	Set Set.instMembership NonemptyChain.carrier Preorder.toLE PartialOrder.toPreorder toPartialOrder	cSup	—	—
map_mem_bot 📖	—	Preorder.toLE PartialOrder.toPreorder toPartialOrder Set Set.instMembership bot	—	—	IsAdmissible.image_self_subset_self bot_isAdmissible Set.mem_image_of_mem
nonempty_fixedPoints_of_inflationary 📖	mathematical	Preorder.toLE PartialOrder.toPreorder toPartialOrder	Set.Nonempty Function.fixedPoints	—	IsAdmissible.base_isLeast bot_isAdmissible IsExtremePt.bot_isChain le_antisymm le_cSup IsAdmissible.image_self_subset_self IsAdmissible.cSup_mem subset_refl Set.instReflSubset
subset_bot_iff 📖	mathematical	IsAdmissible	Set Set.instHasSubset bot	—	subset_antisymm Set.instAntisymmSubset Set.sInter_subset_of_mem subset_refl Set.instReflSubset

ChainCompletePartialOrder.IsAdmissible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
base_isLeast 📖	mathematical	ChainCompletePartialOrder.IsAdmissible	IsLeast Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder	—	—
cSup_mem 📖	mathematical	ChainCompletePartialOrder.IsAdmissible Set Set.instHasSubset SetLike.coe NonemptyChain Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder instSetLikeNonemptyChain	Set.instMembership ChainCompletePartialOrder.cSup	—	—
image_self_subset_self 📖	mathematical	ChainCompletePartialOrder.IsAdmissible	Set Set.instHasSubset Set.image	—	—

ChainCompletePartialOrder.IsExtremePt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_eq_of_le_or_map_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder ChainCompletePartialOrder.IsExtremePt	setOf Set Set.instMembership ChainCompletePartialOrder.bot	—	ChainCompletePartialOrder.subset_bot_iff ChainCompletePartialOrder.IsAdmissible.base_isLeast ChainCompletePartialOrder.bot_isAdmissible mem_bot ChainCompletePartialOrder.map_mem_bot le_iff_lt_or_eq map_le_of_mem_of_lt le_refl le_trans ChainCompletePartialOrder.IsAdmissible.cSup_mem subset_trans Set.instIsTransSubset Set.sep_subset ChainCompletePartialOrder.cSup_le Mathlib.Tactic.Push.not_forall_eq ChainCompletePartialOrder.le_cSup
bot_isChain 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder	IsChain ChainCompletePartialOrder.bot	—	bot_eq_of_le_or_map_le mem_bot_iff_isExtremePt le_trans
map_le_of_mem_of_lt 📖	mathematical	ChainCompletePartialOrder.IsExtremePt Set Set.instMembership ChainCompletePartialOrder.bot Preorder.toLT PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder	Preorder.toLE	—	—
mem_bot 📖	mathematical	ChainCompletePartialOrder.IsExtremePt	Set Set.instMembership ChainCompletePartialOrder.bot	—	—
mem_bot_iff_isExtremePt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder	Set Set.instMembership ChainCompletePartialOrder.bot ChainCompletePartialOrder.IsExtremePt	—	setOf_isExtremePt_eq_bot Set.mem_setOf
setOf_isExtremePt_eq_bot 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder	setOf ChainCompletePartialOrder.IsExtremePt ChainCompletePartialOrder.bot	—	ChainCompletePartialOrder.subset_bot_iff setOf_isExtremePt_isAdmissible mem_bot
setOf_isExtremePt_isAdmissible 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ChainCompletePartialOrder.toPartialOrder	ChainCompletePartialOrder.IsAdmissible setOf ChainCompletePartialOrder.IsExtremePt	—	ChainCompletePartialOrder.IsAdmissible.base_isLeast ChainCompletePartialOrder.bot_isAdmissible lt_irrefl lt_of_le_of_lt mem_bot ChainCompletePartialOrder.map_mem_bot bot_eq_of_le_or_map_le le_iff_lt_or_eq le_trans map_le_of_mem_of_lt le_refl lt_of_lt_of_le ChainCompletePartialOrder.IsAdmissible.cSup_mem subset_trans Set.instIsTransSubset ChainCompletePartialOrder.cSup_le Mathlib.Tactic.Push.not_and_eq ChainCompletePartialOrder.le_cSup

NonemptyChain

Definitions

Name	Category	Theorems
carrier 📖	CompOp	3 math math: ext_iff, Nonempty', isChain'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Nonempty' 📖	mathematical	—	Set.Nonempty carrier	—	—
ext 📖	—	carrier	—	—	—
ext_iff 📖	mathematical	—	carrier	—	ext
isChain' 📖	mathematical	—	IsChain carrier	—	—

(root)

Definitions

Name	Category	Theorems
ChainCompletePartialOrder 📖	CompData	—
NonemptyChain 📖	CompData	—
instPartialOrderNonemptyChain 📖	CompOp	—
instSetLikeNonemptyChain 📖	CompOp	—

---

← Back to Index