Documentation Verification Report

Directed

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

Statistics

Metric	Count
Definitions `iSupLift`	1
Theorems `coe_iSup_of_directed`, `iSupLift_comp_inclusion`, `iSupLift_inclusion`, `iSupLift_mk`, `iSupLift_of_mem`	5
Total	6

Subalgebra

Definitions

Name	Category	Theorems
`iSupLift` 📖	CompOp	4 math math: `iSupLift_mk`, `iSupLift_of_mem`, `iSupLift_comp_inclusion`, `iSupLift_inclusion`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_iSup_of_directed` 📖	mathematical	`Directed` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra` `Set.iUnion`	—	`Subsemiring.coe_iSup_of_directed` `Set.mem_iUnion` `algebraMap_mem` `le_antisymm` `iSup_le` `le_iSup` `Set.iUnion_subset`
`iSupLift_comp_inclusion` 📖	mathematical	`Directed` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AlgHom.comp` `SetLike.instMembership` `instSetLike` `toSemiring` `algebra` `inclusion` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	`iSupLift`	—	`AlgHom.ext` `iSupLift_inclusion`
`iSupLift_inclusion` 📖	mathematical	`Directed` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AlgHom.comp` `SetLike.instMembership` `instSetLike` `toSemiring` `algebra` `inclusion` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `iSupLift`	—	`SetLike.coe_subset_coe` `instIsConcreteLE` `LE.le.trans` `Set.iUnionLift_inclusion`
`iSupLift_mk` 📖	mathematical	`Directed` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AlgHom.comp` `SetLike.instMembership` `instSetLike` `toSemiring` `algebra` `inclusion` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `iSupLift`	—	—
`iSupLift_of_mem` 📖	mathematical	`Directed` `Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AlgHom.comp` `SetLike.instMembership` `instSetLike` `toSemiring` `algebra` `inclusion` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Algebra.instCompleteLatticeSubalgebra`	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `iSupLift`	—	`Set.iUnionLift_of_mem`

---

← Back to Index