Documentation Verification Report

Relative

📁 Source: Mathlib/Order/UpperLower/Relative.lean

Statistics

Metric	Count
Definitions `instPartialOrderRelUpperSet`, `instSetLikeRelLowerSet`, `instSetLikeRelUpperSet`	3
Theorems `isRelLowerSet_sep`, `iInter`, `iInter₂`, `iUnion`, `iUnion₂`, `inter`, `mem_of_le`, `mono_isLowerSet`, `prop_of_mem`, `sInter`, `sUnion`, `union`, `iInter`, `iInter₂`, `iUnion`, `iUnion₂`, `inter`, `mem_of_le`, `mono_isUpperSet`, `prop_of_mem`, `sInter`, `sUnion`, `union`, `isRelUpperSet_sep`, `isRelLowerSet`, `isRelUpperSet`, `isLowerSet_subtype_iff_isRelLowerSet`, `isRelLowerSet_Icc_ge`, `isRelLowerSet_empty`, `isRelLowerSet_self`, `isRelLowerSet_true_iff_isLowerSet`, `isRelUpperSet_Icc_le`, `isRelUpperSet_empty`, `isRelUpperSet_self`, `isRelUpperSet_true_iff_isUpperSet`, `isUpperSet_subtype_iff_isRelUpperSet`	36
Total	39

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRelLowerSet_sep` 📖	mathematical	`IsLowerSet`	`IsRelLowerSet` `setOf` `Set` `Set.instMembership`	—	—

IsRelLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInter` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set.iInter`	—	`sInter` `Set.range_nonempty` `Set.forall_mem_range`
`iInter₂` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set.iInter`	—	`iInter`
`iUnion` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set.iUnion`	—	`sUnion` `Set.forall_mem_range`
`iUnion₂` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set.iUnion`	—	`iUnion`
`inter` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set` `Set.instInter`	—	—
`mem_of_le` 📖	mathematical	`IsRelLowerSet` `Set` `Set.instMembership`	`Set` `Set.instMembership`	—	—
`mono_isLowerSet` 📖	mathematical	`IsRelLowerSet` `IsLowerSet` `Set` `Set.instHasSubset`	`IsRelLowerSet`	—	—
`prop_of_mem` 📖	—	`IsRelLowerSet` `Set` `Set.instMembership`	—	—	—
`sInter` 📖	mathematical	`Set.Nonempty` `Set` `IsRelLowerSet`	`IsRelLowerSet` `Set.sInter`	—	—
`sUnion` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set.sUnion`	—	—
`union` 📖	mathematical	`IsRelLowerSet`	`IsRelLowerSet` `Set` `Set.instUnion`	—	—

IsRelUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInter` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set.iInter`	—	`sInter` `Set.range_nonempty` `Set.forall_mem_range`
`iInter₂` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set.iInter`	—	`iInter`
`iUnion` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set.iUnion`	—	`sUnion` `Set.forall_mem_range`
`iUnion₂` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set.iUnion`	—	`iUnion`
`inter` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set` `Set.instInter`	—	—
`mem_of_le` 📖	mathematical	`IsRelUpperSet` `Set` `Set.instMembership`	`Set` `Set.instMembership`	—	—
`mono_isUpperSet` 📖	mathematical	`IsRelUpperSet` `IsUpperSet` `Set` `Set.instHasSubset`	`IsRelUpperSet`	—	—
`prop_of_mem` 📖	—	`IsRelUpperSet` `Set` `Set.instMembership`	—	—	—
`sInter` 📖	mathematical	`Set.Nonempty` `Set` `IsRelUpperSet`	`IsRelUpperSet` `Set.sInter`	—	—
`sUnion` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set.sUnion`	—	—
`union` 📖	mathematical	`IsRelUpperSet`	`IsRelUpperSet` `Set` `Set.instUnion`	—	—

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRelUpperSet_sep` 📖	mathematical	`IsUpperSet`	`IsRelUpperSet` `setOf` `Set` `Set.instMembership`	—	—

RelLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRelLowerSet` 📖	mathematical	—	`IsRelLowerSet` `SetLike.coe` `RelLowerSet` `instSetLikeRelLowerSet`	—	`isRelLowerSet'`

RelUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isRelUpperSet` 📖	mathematical	—	`IsRelUpperSet` `SetLike.coe` `RelUpperSet` `instSetLikeRelUpperSet`	—	`isRelUpperSet'`

(root)

Definitions

Name	Category	Theorems
`instPartialOrderRelUpperSet` 📖	CompOp	—
`instSetLikeRelLowerSet` 📖	CompOp	1 math math: `RelLowerSet.isRelLowerSet`
`instSetLikeRelUpperSet` 📖	CompOp	1 math math: `RelUpperSet.isRelUpperSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLowerSet_subtype_iff_isRelLowerSet` 📖	mathematical	—	`IsLowerSet` `IsRelLowerSet` `Set.image`	—	`Subtype.coe_eta`
`isRelLowerSet_Icc_ge` 📖	mathematical	—	`IsRelLowerSet` `Preorder.toLE` `Set.Icc`	—	`LE.le.trans`
`isRelLowerSet_empty` 📖	mathematical	—	`IsRelLowerSet` `Set` `Set.instEmptyCollection`	—	—
`isRelLowerSet_self` 📖	mathematical	—	`IsRelLowerSet` `Set` `Set.instMembership`	—	—
`isRelLowerSet_true_iff_isLowerSet` 📖	mathematical	—	`IsRelLowerSet` `IsLowerSet`	—	—
`isRelUpperSet_Icc_le` 📖	mathematical	—	`IsRelUpperSet` `Preorder.toLE` `Set.Icc`	—	`LE.le.trans`
`isRelUpperSet_empty` 📖	mathematical	—	`IsRelUpperSet` `Set` `Set.instEmptyCollection`	—	—
`isRelUpperSet_self` 📖	mathematical	—	`IsRelUpperSet` `Set` `Set.instMembership`	—	—
`isRelUpperSet_true_iff_isUpperSet` 📖	mathematical	—	`IsRelUpperSet` `IsUpperSet`	—	—
`isUpperSet_subtype_iff_isRelUpperSet` 📖	mathematical	—	`IsUpperSet` `IsRelUpperSet` `Set.image`	—	`Subtype.coe_eta`

---

← Back to Index