Documentation Verification Report

Defs

📁 Source: Mathlib/Logic/Nontrivial/Defs.lean

Statistics

Metric	Count
Definitions	0
Theorems `instNontrivial`, `exists_ne`, `exists_ne`, `nontrivial`, `nontrivial`, `nontrivial_of_nontrivial`, `exists_pair_ne`, `to_nonempty`, `exists_ne`, `exists_pair_ne`, `false_of_nontrivial_of_subsingleton`, `instNontrivialProp`, `nontrivial_iff`, `nontrivial_iff_exists_ne`, `nontrivial_of_ne`, `not_nontrivial`, `not_nontrivial_iff_subsingleton`, `not_subsingleton`, `not_subsingleton_iff_nontrivial`, `subsingleton_iff`, `subsingleton_or_nontrivial`	21
Total	21

Bool

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNontrivial` 📖	mathematical	—	`Nontrivial`	—	—

Decidable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ne` 📖	—	—	—	—	`exists_pair_ne`

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nontrivial_of_nontrivial` 📖	mathematical	—	`Nontrivial`	—	`exists_pair_ne` `nontrivial_of_ne`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ne` 📖	—	—	—	—	`exists_pair_ne`
`nontrivial` 📖	mathematical	—	`Nontrivial`	—	`exists_pair_ne`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nontrivial` 📖	mathematical	—	`Nontrivial`	—	`exists_pair_ne`

Nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pair_ne` 📖	—	—	—	—	—
`to_nonempty` 📖	—	—	—	—	`exists_pair_ne`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ne` 📖	—	—	—	—	`Decidable.exists_ne`
`exists_pair_ne` 📖	—	—	—	—	`Nontrivial.exists_pair_ne`
`false_of_nontrivial_of_subsingleton` 📖	—	—	—	—	`not_nontrivial`
`instNontrivialProp` 📖	mathematical	—	`Nontrivial`	—	—
`nontrivial_iff` 📖	mathematical	—	`Nontrivial`	—	`Nontrivial.exists_pair_ne`
`nontrivial_iff_exists_ne` 📖	mathematical	—	`Nontrivial`	—	`exists_ne` `nontrivial_of_ne`
`nontrivial_of_ne` 📖	mathematical	—	`Nontrivial`	—	—
`not_nontrivial` 📖	mathematical	—	`Nontrivial`	—	—
`not_nontrivial_iff_subsingleton` 📖	mathematical	—	`Nontrivial`	—	—
`not_subsingleton` 📖	—	—	—	—	`not_nontrivial`
`not_subsingleton_iff_nontrivial` 📖	mathematical	—	`Nontrivial`	—	`not_nontrivial_iff_subsingleton`
`subsingleton_iff` 📖	—	—	—	—	—
`subsingleton_or_nontrivial` 📖	mathematical	—	`Nontrivial`	—	`not_nontrivial_iff_subsingleton`

---

← Back to Index