Documentation Verification Report

Relator

📁 Source: Mathlib/Logic/Relator.lean

Statistics

Metric	Count
Definitions `BiTotal`, `BiUnique`, `LeftTotal`, `LeftUnique`, `LiftFun`, `RightTotal`, `RightUnique`, `«term_⇒_»`	8
Theorems `refl`, `rel_exists`, `rel_forall`, `trans`, `refl`, `rel_exists`, `trans`, `flip`, `refl`, `rel_forall`, `trans`, `bi_total_eq`, `left_unique_of_rel_eq`, `rel_and`, `rel_eq`, `rel_iff`, `rel_imp`, `rel_not`, `rel_or`	19
Total	27

Relator

Definitions

Name	Category	Theorems
`BiTotal` 📖	MathDef	6 math math: `biTotal_iff_isEmpty_left`, `bi_total_eq`, `biTotal_empty`, `BiTotal.refl`, `SetTheory.PGame.identical_iff`, `biTotal_iff_isEmpty_right`
`BiUnique` 📖	MathDef	—
`LeftTotal` 📖	MathDef	4 math math: `RightTotal.symm`, `leftTotal_empty`, `leftTotal_iff_isEmpty_left`, `LeftTotal.refl`
`LeftUnique` 📖	MathDef	4 math math: `Option.Mem.leftUnique`, `Part.Mem.left_unique`, `Computation.Mem.left_unique`, `left_unique_of_rel_eq`
`LiftFun` 📖	MathDef	28 math math: `BiTotal.rel_forall`, `Fin.liftFun_iff_succ`, `rel_imp`, `RightTotal.rel_forall`, `List.rel_filterMap`, `List.rel_perm`, `List.rel_foldl`, `rel_not`, `Subgroup.prod_mono`, `List.rel_map`, `LeftTotal.rel_exists`, `List.rel_foldr`, `List.rel_reverse`, `liftFun_vecCons`, `List.rel_nodup`, `BiTotal.rel_exists`, `AddConstMapClass.rel_map_of_Icc`, `List.rel_flatMap`, `AddSubgroup.prod_mono`, `rel_iff`, `List.rel_append`, `List.rel_mem`, `rel_or`, `List.rel_flatten`, `List.rel_perm_imp`, `List.rel_sections`, `rel_eq`, `rel_and`
`RightTotal` 📖	MathDef	4 math math: `rightTotal_iff_isEmpty_right`, `rightTotal_empty`, `RightTotal.refl`, `LeftTotal.symm`
`RightUnique` 📖	MathDef	2 math math: `Part.Mem.right_unique`, `LeftUnique.flip`
`«term_⇒_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bi_total_eq` 📖	mathematical	—	`BiTotal`	—	—
`left_unique_of_rel_eq` 📖	mathematical	`LiftFun`	`LeftUnique`	—	—
`rel_and` 📖	mathematical	—	`LiftFun`	—	—
`rel_eq` 📖	mathematical	`BiUnique`	`LiftFun`	—	—
`rel_iff` 📖	mathematical	—	`LiftFun`	—	—
`rel_imp` 📖	mathematical	—	`LiftFun`	—	—
`rel_not` 📖	mathematical	—	`LiftFun`	—	—
`rel_or` 📖	mathematical	—	`LiftFun`	—	—

Relator.BiTotal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Relator.BiTotal`	—	`Relator.LeftTotal.refl` `Relator.RightTotal.refl`
`rel_exists` 📖	mathematical	`Relator.BiTotal`	`Relator.LiftFun`	—	—
`rel_forall` 📖	mathematical	`Relator.BiTotal`	`Relator.LiftFun`	—	—
`trans` 📖	—	`Relator.BiTotal`	—	—	`Relator.LeftTotal.trans` `Relator.RightTotal.trans`

Relator.LeftTotal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Relator.LeftTotal`	—	—
`rel_exists` 📖	mathematical	`Relator.LeftTotal`	`Relator.LiftFun`	—	—
`trans` 📖	—	`Relator.LeftTotal`	—	—	—

Relator.LeftUnique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`flip` 📖	mathematical	`Relator.LeftUnique`	`Relator.RightUnique`	—	—

Relator.RightTotal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Relator.RightTotal`	—	`Relator.LeftTotal.refl`
`rel_forall` 📖	mathematical	`Relator.RightTotal`	`Relator.LiftFun`	—	—
`trans` 📖	—	`Relator.RightTotal`	—	—	`Relator.LeftTotal.trans`

---

← Back to Index