Radical

📁 Source: Mathlib/Order/Radical.lean

Statistics

Metric	Count
Definitions radical	1
Theorems radical_le_coatom, radical_nongenerating, map_radical	3
Total	4

Order

Definitions

Name	Category	Theorems
radical 📖	CompOp	2 math math: OrderIso.map_radical, radical_le_coatom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
radical_le_coatom 📖	mathematical	IsCoatom PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder	radical ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	biInf_le
radical_nongenerating 📖	—	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice radical PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Top.top OrderTop.toTop SemilatticeSup.toPartialOrder CompleteLattice.toLattice	—	—	IsCoatomic.eq_top_or_exists_le_coatom sup_le radical_le_coatom top_le_iff

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_radical 📖	mathematical	—	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instFunLikeOrderIso Order.radical BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	map_iInf Equiv.iInf_congr iInf_congr_Prop

---

← Back to Index