Documentation Verification Report

UnionLift

📁 Source: Mathlib/Data/Set/UnionLift.lean

Statistics

Metric	Count
Definitions `iUnionLift`, `liftCover`	2
Theorems `iUnionLift_binary`, `iUnionLift_const`, `iUnionLift_inclusion`, `iUnionLift_mk`, `iUnionLift_of_mem`, `iUnionLift_unary`, `liftCover_coe`, `liftCover_of_mem`, `preimage_iUnionLift`, `preimage_liftCover`	10
Total	12

Set

Definitions

Name	Category	Theorems
`iUnionLift` 📖	CompOp	8 math math: `measurable_iUnionLift`, `iUnionLift_unary`, `iUnionLift_of_mem`, `iUnionLift_mk`, `iUnionLift_inclusion`, `iUnionLift_const`, `iUnionLift_binary`, `preimage_iUnionLift`
`liftCover` 📖	CompOp	4 math math: `liftCover_coe`, `liftCover_of_mem`, `measurable_liftCover`, `preimage_liftCover`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iUnionLift_binary` 📖	mathematical	`Set` `instMembership` `iUnion` `Directed` `instLE` `inclusion`	`iUnionLift` `le_of_eq` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`subset_iUnion` `le_of_eq` `mem_iUnion` `Subtype.prop` `iUnionLift_of_mem`
`iUnionLift_const` 📖	mathematical	`Set` `instMembership` `instHasSubset` `iUnion`	`iUnionLift`	—	`mem_iUnion` `Subtype.prop` `iUnionLift_of_mem`
`iUnionLift_inclusion` 📖	mathematical	`Set` `instMembership` `instHasSubset` `iUnion`	`iUnionLift` `inclusion`	—	—
`iUnionLift_mk` 📖	mathematical	`Set` `instMembership` `instHasSubset` `iUnion`	`iUnionLift`	—	—
`iUnionLift_of_mem` 📖	mathematical	`Set` `instMembership` `instHasSubset` `iUnion`	`iUnionLift`	—	—
`iUnionLift_unary` 📖	mathematical	`Set` `instMembership` `iUnion` `inclusion`	`iUnionLift` `le_of_eq` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra`	—	`subset_iUnion` `le_of_eq` `mem_iUnion` `Subtype.prop` `iUnionLift_of_mem` `iUnionLift_inclusion`
`liftCover_coe` 📖	mathematical	`Set` `instMembership` `iUnion` `univ`	`liftCover`	—	—
`liftCover_of_mem` 📖	mathematical	`Set` `instMembership` `iUnion` `univ`	`liftCover`	—	`iUnionLift_of_mem`
`preimage_iUnionLift` 📖	mathematical	`Set` `instMembership` `instHasSubset` `iUnion`	`preimage` `Elem` `iUnionLift` `inclusion` `image` `subset_iUnion`	—	`ext` `subset_iUnion` `mem_iUnion` `Subtype.prop` `iUnionLift_of_mem`
`preimage_liftCover` 📖	mathematical	`Set` `instMembership` `iUnion` `univ`	`preimage` `liftCover` `image` `Elem`	—	`Eq.subset` `instReflSubset` `mem_univ` `preimage_comp` `subset_iUnion` `preimage_iUnionLift` `ext`

---

← Back to Index