Basic

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

Statistics

Metric	Count
Definitions nontrivialPSumUnique	1
Theorems nontrivial, nontrivial, nontrivial, nontrivial_at, le, nontrivial_iff_exists_ne, exists_pair_lt, nontrivial_iff_lt, nontrivial_of_lt, nontrivial_prod_left, nontrivial_prod_right	11
Total	12

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nontrivial 📖	mathematical	—	Nontrivial	—	Pi.nontrivial_at Nontrivial.to_nonempty

Option

Theorems

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

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nontrivial 📖	mathematical	—	Nontrivial	—	nontrivial_at
nontrivial_at 📖	mathematical	—	Nontrivial	—	Function.Injective.nontrivial Function.update_injective

Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le 📖	mathematical	—	Preorder.toLE	—	le_of_eq

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nontrivial_iff_exists_ne 📖	mathematical	—	Nontrivial	—	nontrivial_iff_exists_ne

(root)

Definitions

Name	Category	Theorems
nontrivialPSumUnique 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_pair_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	exists_pair_ne lt_or_gt_of_ne
nontrivial_iff_lt 📖	mathematical	—	Nontrivial Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	exists_pair_lt nontrivial_of_lt
nontrivial_of_lt 📖	mathematical	Preorder.toLT	Nontrivial	—	ne_of_lt
nontrivial_prod_left 📖	mathematical	—	Nontrivial	—	Function.Surjective.nontrivial Prod.fst_surjective
nontrivial_prod_right 📖	mathematical	—	Nontrivial	—	Function.Surjective.nontrivial Prod.snd_surjective

---

← Back to Index