Documentation Verification Report

Find

📁 Source: Mathlib/Data/PNat/Find.lean

Statistics

Metric	Count
Definitions `decidablePredExistsNat`, `find`, `findX`	3
Theorems `find_comp_succ`, `find_eq_iff`, `find_eq_one`, `find_le`, `find_le_iff`, `find_lt_iff`, `find_min`, `find_min'`, `find_mono`, `find_spec`, `le_find_iff`, `lt_find_iff`, `one_le_find`	13
Total	16

PNat

Definitions

Name	Category	Theorems
`decidablePredExistsNat` 📖	CompOp	—
`find` 📖	CompOp	12 math math: `find_le`, `find_spec`, `find_mono`, `find_le_iff`, `find_comp_succ`, `find_lt_iff`, `find_eq_one`, `find_min'`, `lt_find_iff`, `one_le_find`, `find_eq_iff`, `le_find_iff`
`findX` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`find_comp_succ` 📖	mathematical	`PNat` `instAddPNat` `instOfNatPNatOfNeZeroNat`	`find`	—	`find_eq_iff` `find_spec` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `addLeftMono` `contravariant_swap_add_of_contravariant_add` `addLeftReflectLT` `le_rfl`
`find_eq_iff` 📖	mathematical	—	`find`	—	`find_spec` `find_min` `le_antisymm` `find_min'` `not_lt`
`find_eq_one` 📖	mathematical	—	`find` `PNat` `instOfNatPNatOfNeZeroNat`	—	`instIsEmptyFalse`
`find_le` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	`find_le_iff` `le_rfl`
`find_le_iff` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	—
`find_lt_iff` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	`find_spec` `LE.le.trans_lt` `find_min'`
`find_min` 📖	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	—	`Subtype.prop`
`find_min'` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	`le_of_not_gt` `find_min`
`find_mono` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	`find_min'` `find_spec`
`find_spec` 📖	mathematical	—	`find`	—	`Subtype.prop`
`le_find_iff` 📖	mathematical	—	`PNat` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	—
`lt_find_iff` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `find`	—	`covariant_swap_add_of_covariant_add` `addLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `addLeftReflectLT`
`one_le_find` 📖	mathematical	—	`PNat` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderPNat` `instOfNatPNatOfNeZeroNat` `find`	—	—

---

← Back to Index