Pi

Statistics

Metric	Count
Definitions	0
Theorems `exists_forall_pos_add_lt`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_forall_pos_add_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`nonempty_fintype` `isEmpty_or_nonempty` `exists_ne` `Ne.lt_or_gt` `exists_pos_add_of_lt'` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `Finset.univ_nonempty` `Finset.lt_inf'_iff` `exists_between` `add_lt_add_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `LT.lt.trans_le` `Finset.inf'_le` `Finset.mem_univ`

---