PartENat

📁 Source: Mathlib/Data/Nat/PartENat.lean

Statistics

Metric	Count
Definitions `PartENat`, `addCommMonoid`, `boundedOrder`, `decidableLe`, `find`, `instAdd`, `instAddCommMonoidWithOne`, `instBot`, `instCoeENat`, `instCompleteLinearOrder`, `instDecidableDomNatSome`, `instInhabited`, `instLE`, `instLinearOrderedAddCommMonoidWithTop`, `instMax`, `instOne`, `instTop`, `instZero`, `lattice`, `linearOrder`, `ofENat`, `orderBot`, `orderTop`, `partialOrder`, `semilatticeSup`, `some`, `toWithTop`, `wellFoundedRelation`, `withTopAddEquiv`, `withTopEquiv`, `withTopOrderIso`	31
Theorems `add_eq_top_iff`, `add_left_cancel_iff`, `add_lt_add_iff_left`, `add_lt_add_iff_right`, `add_lt_add_right`, `add_one_le_iff_lt`, `add_one_le_of_lt`, `add_right_cancel_iff`, `add_top`, `casesOn`, `casesOn'`, `coe_add_get`, `coe_le_coe`, `coe_le_iff`, `coe_lt_coe`, `coe_lt_iff`, `coe_succ_le_iff`, `dom_natCast`, `dom_ofNat`, `dom_of_le_natCast`, `dom_of_le_of_dom`, `dom_of_le_some`, `dom_of_lt`, `dom_one`, `dom_some`, `dom_zero`, `eq_natCast_sub_of_add_eq_natCast`, `eq_top_iff_forall_le`, `eq_top_iff_forall_lt`, `eq_zero_iff`, `find_dom`, `find_eq_top_iff`, `find_get`, `find_le`, `get_add`, `get_eq_iff_eq_coe`, `get_eq_iff_eq_some`, `get_le_get`, `get_natCast`, `get_natCast'`, `get_ofNat'`, `get_one`, `get_zero`, `instCanLiftNatCastDom`, `instCanonicallyOrderedAdd`, `instCharZero`, `instWellFoundedLT`, `instZeroLEOneClass`, `isOrderedAddMonoid`, `isTotal`, `le_coe_iff`, `le_def`, `le_of_lt_add_one`, `lt_add_iff_pos_right`, `lt_add_one`, `lt_add_one_iff_lt`, `lt_coe_iff`, `lt_coe_succ_iff_le`, `lt_def`, `lt_find`, `lt_find_iff`, `lt_wf`, `natCast_get`, `natCast_inj`, `natCast_lt_top`, `natCast_ne_top`, `ne_top_iff`, `ne_top_iff_dom`, `ne_top_of_lt`, `ne_zero_iff`, `not_dom_iff_eq_top`, `not_isMax_natCast`, `ofENat_coe`, `ofENat_le`, `ofENat_lt`, `ofENat_ofNat`, `ofENat_one`, `ofENat_toWithTop`, `ofENat_top`, `ofENat_zero`, `ofNat_lt_top`, `ofNat_ne_top`, `one_lt_top`, `one_ne_top`, `pos_iff_one_le`, `some_eq_natCast`, `toWithTop_add`, `toWithTop_le`, `toWithTop_lt`, `toWithTop_natCast`, `toWithTop_natCast'`, `toWithTop_ofENat`, `toWithTop_ofNat`, `toWithTop_one`, `toWithTop_one'`, `toWithTop_some`, `toWithTop_top`, `toWithTop_top'`, `toWithTop_zero`, `toWithTop_zero'`, `top_add`, `top_eq_none`, `withTopEquiv_apply`, `withTopEquiv_le`, `withTopEquiv_lt`, `withTopEquiv_natCast`, `withTopEquiv_ofNat`, `withTopEquiv_one`, `withTopEquiv_symm_apply`, `withTopEquiv_symm_coe`, `withTopEquiv_symm_le`, `withTopEquiv_symm_lt`, `withTopEquiv_symm_ofNat`, `withTopEquiv_symm_one`, `withTopEquiv_symm_top`, `withTopEquiv_symm_zero`, `withTopEquiv_top`, `withTopEquiv_zero`, `zero_lt_top`, `zero_ne_top`	120
Total	151

PartENat

Definitions

Name	Category	Theorems
`addCommMonoid` 📖	CompOp	1 math math: `isOrderedAddMonoid`
`boundedOrder` 📖	CompOp	—
`decidableLe` 📖	CompOp	—
`find` 📖	CompOp	5 math math: `lt_find_iff`, `find_eq_top_iff`, `find_le`, `lt_find`, `find_dom`
`instAdd` 📖	CompOp	15 math math: `top_add`, `instCanonicallyOrderedAdd`, `add_one_le_iff_lt`, `lt_add_one_iff_lt`, `add_top`, `toWithTop_add`, `add_one_le_of_lt`, `add_right_cancel_iff`, `add_lt_add_iff_right`, `add_eq_top_iff`, `lt_add_iff_pos_right`, `add_lt_add_iff_left`, `add_lt_add_right`, `lt_add_one`, `add_left_cancel_iff`
`instAddCommMonoidWithOne` 📖	CompOp	31 math math: `toWithTop_natCast`, `lt_find_iff`, `coe_lt_coe`, `lt_coe_iff`, `get_natCast`, `le_coe_iff`, `not_isMax_natCast`, `withTopEquiv_symm_ofNat`, `ofENat_ofNat`, `instCanLiftNatCastDom`, `natCast_get`, `dom_natCast`, `find_le`, `toWithTop_natCast'`, `eq_top_iff_forall_le`, `natCast_lt_top`, `withTopEquiv_natCast`, `coe_le_coe`, `eq_top_iff_forall_lt`, `coe_succ_le_iff`, `coe_lt_iff`, `get_eq_iff_eq_coe`, `ofENat_coe`, `ne_top_iff`, `some_eq_natCast`, `coe_le_iff`, `withTopEquiv_symm_coe`, `lt_find`, `natCast_inj`, `lt_coe_succ_iff_le`, `instCharZero`
`instBot` 📖	CompOp	1 math math: `ne_zero_iff`
`instCoeENat` 📖	CompOp	—
`instCompleteLinearOrder` 📖	CompOp	—
`instDecidableDomNatSome` 📖	CompOp	1 math math: `toWithTop_some`
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	23 math math: `ofENat_le`, `instCanonicallyOrderedAdd`, `eq_zero_iff`, `pos_iff_one_le`, `add_one_le_iff_lt`, `le_coe_iff`, `lt_add_one_iff_lt`, `not_isMax_natCast`, `get_le_get`, `toWithTop_le`, `add_one_le_of_lt`, `le_of_lt_add_one`, `find_le`, `eq_top_iff_forall_le`, `le_def`, `coe_le_coe`, `instZeroLEOneClass`, `coe_succ_le_iff`, `withTopEquiv_le`, `isTotal`, `withTopEquiv_symm_le`, `coe_le_iff`, `lt_coe_succ_iff_le`
`instLinearOrderedAddCommMonoidWithTop` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instOne` 📖	CompOp	13 math math: `dom_one`, `ofENat_one`, `withTopEquiv_one`, `pos_iff_one_le`, `add_one_le_iff_lt`, `lt_add_one_iff_lt`, `one_lt_top`, `add_one_le_of_lt`, `toWithTop_one`, `withTopEquiv_symm_one`, `instZeroLEOneClass`, `toWithTop_one'`, `lt_add_one`
`instTop` 📖	CompOp	17 math math: `top_add`, `ofNat_lt_top`, `top_eq_none`, `not_dom_iff_eq_top`, `add_top`, `one_lt_top`, `find_eq_top_iff`, `eq_top_iff_forall_le`, `natCast_lt_top`, `eq_top_iff_forall_lt`, `toWithTop_top`, `withTopEquiv_top`, `toWithTop_top'`, `add_eq_top_iff`, `zero_lt_top`, `ofENat_top`, `withTopEquiv_symm_top`
`instZero` 📖	CompOp	11 math math: `eq_zero_iff`, `pos_iff_one_le`, `toWithTop_zero'`, `instZeroLEOneClass`, `toWithTop_zero`, `dom_zero`, `lt_add_iff_pos_right`, `withTopEquiv_symm_zero`, `zero_lt_top`, `withTopEquiv_zero`, `ofENat_zero`
`lattice` 📖	CompOp	—
`linearOrder` 📖	CompOp	—
`ofENat` 📖	CompOp	10 math math: `ofENat_le`, `withTopEquiv_symm_apply`, `ofENat_one`, `ofENat_ofNat`, `ofENat_lt`, `ofENat_coe`, `ofENat_zero`, `toWithTop_ofENat`, `ofENat_top`, `ofENat_toWithTop`
`orderBot` 📖	CompOp	—
`orderTop` 📖	CompOp	—
`partialOrder` 📖	CompOp	29 math math: `eq_natCast_sub_of_add_eq_natCast`, `lt_find_iff`, `coe_lt_coe`, `lt_coe_iff`, `pos_iff_one_le`, `add_one_le_iff_lt`, `ofNat_lt_top`, `instWellFoundedLT`, `toWithTop_lt`, `lt_add_one_iff_lt`, `lt_def`, `one_lt_top`, `isOrderedAddMonoid`, `ne_zero_iff`, `natCast_lt_top`, `eq_top_iff_forall_lt`, `coe_succ_le_iff`, `coe_lt_iff`, `add_lt_add_iff_right`, `ofENat_lt`, `withTopEquiv_lt`, `lt_add_iff_pos_right`, `lt_wf`, `add_lt_add_iff_left`, `zero_lt_top`, `lt_add_one`, `lt_find`, `lt_coe_succ_iff_le`, `withTopEquiv_symm_lt`
`semilatticeSup` 📖	CompOp	—
`some` 📖	CompOp	4 math math: `get_eq_iff_eq_some`, `dom_some`, `toWithTop_some`, `some_eq_natCast`
`toWithTop` 📖	CompOp	16 math math: `toWithTop_natCast`, `toWithTop_lt`, `toWithTop_zero'`, `toWithTop_add`, `toWithTop_le`, `toWithTop_one`, `toWithTop_natCast'`, `toWithTop_top`, `toWithTop_top'`, `toWithTop_zero`, `withTopEquiv_apply`, `toWithTop_some`, `toWithTop_one'`, `toWithTop_ofNat`, `toWithTop_ofENat`, `ofENat_toWithTop`
`wellFoundedRelation` 📖	CompOp	—
`withTopAddEquiv` 📖	CompOp	—
`withTopEquiv` 📖	CompOp	16 math math: `withTopEquiv_symm_apply`, `withTopEquiv_one`, `withTopEquiv_ofNat`, `withTopEquiv_symm_ofNat`, `withTopEquiv_symm_one`, `withTopEquiv_natCast`, `withTopEquiv_top`, `withTopEquiv_le`, `withTopEquiv_lt`, `withTopEquiv_apply`, `withTopEquiv_symm_zero`, `withTopEquiv_zero`, `withTopEquiv_symm_le`, `withTopEquiv_symm_coe`, `withTopEquiv_symm_lt`, `withTopEquiv_symm_top`
`withTopOrderIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_eq_top_iff` 📖	mathematical	—	`PartENat` `instAdd` `Top.top` `instTop`	—	`add_top` `top_add`
`add_left_cancel_iff` 📖	mathematical	—	`PartENat` `instAdd`	—	`add_comm` `add_right_cancel_iff`
`add_lt_add_iff_left` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instAdd`	—	`add_comm` `add_lt_add_iff_right`
`add_lt_add_iff_right` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instAdd`	—	`lt_of_add_lt_add_right` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `add_lt_add_right`
`add_lt_add_right` 📖	mathematical	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`instAdd`	—	`ne_top_iff` `ne_top_of_lt` `top_add` `natCast_lt_top` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid`
`add_one_le_iff_lt` 📖	mathematical	—	`PartENat` `instLE` `instAdd` `instOne` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`ne_top_iff` `natCast_lt_top` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero` `Nat.cast_one` `add_one_le_of_lt`
`add_one_le_of_lt` 📖	mathematical	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`instLE` `instAdd` `instOne`	—	`le_top` `ne_top_iff` `ne_top_of_lt` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero`
`add_right_cancel_iff` 📖	mathematical	—	`PartENat` `instAdd`	—	`ne_top_iff` `top_add` `instCharZero` `add_comm` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`add_top` 📖	mathematical	—	`PartENat` `instAdd` `Top.top` `instTop`	—	`add_comm` `top_add`
`casesOn` 📖	—	`Top.top` `PartENat` `instTop` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—	`casesOn'`
`casesOn'` 📖	—	`Top.top` `PartENat` `instTop` `some`	—	—	`Part.induction_on`
`coe_add_get` 📖	mathematical	`Part.Dom` `PartENat` `instAdd` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	`Part.get`	—	—
`coe_le_coe` 📖	mathematical	—	`PartENat` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero`
`coe_le_iff` 📖	mathematical	—	`PartENat` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Part.get`	—	`some_eq_natCast`
`coe_lt_coe` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero`
`coe_lt_iff` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Part.get`	—	`some_eq_natCast`
`coe_succ_le_iff` 📖	mathematical	—	`PartENat` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`Nat.cast_add` `Nat.cast_one` `add_one_le_iff_lt` `natCast_ne_top`
`dom_natCast` 📖	mathematical	—	`Part.Dom` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`dom_ofNat` 📖	mathematical	—	`Part.Dom`	—	—
`dom_of_le_natCast` 📖	mathematical	`PartENat` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	`Part.Dom`	—	`dom_of_le_some`
`dom_of_le_of_dom` 📖	—	`PartENat` `instLE` `Part.Dom`	—	—	—
`dom_of_le_some` 📖	mathematical	`PartENat` `instLE` `some`	`Part.Dom`	—	`dom_of_le_of_dom`
`dom_of_lt` 📖	mathematical	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	`Part.Dom`	—	`not_top_lt` `dom_natCast`
`dom_one` 📖	mathematical	—	`Part.Dom` `PartENat` `instOne`	—	—
`dom_some` 📖	mathematical	—	`Part.Dom` `some`	—	—
`dom_zero` 📖	mathematical	—	`Part.Dom` `PartENat` `instZero`	—	—
`eq_natCast_sub_of_add_eq_natCast` 📖	mathematical	`PartENat` `instAdd` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	`Part.get` `dom_of_le_natCast` `LE.le.trans_eq` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `le_add_left` `instCanonicallyOrderedAdd` `le_rfl`	—	`dom_of_le_natCast` `LE.le.trans_eq` `le_add_left` `instCanonicallyOrderedAdd` `le_rfl` `CanLift.prf` `instCanLiftNatCastDom` `le_add_right` `dom_natCast` `get_natCast` `eq_tsub_of_add_eq` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.cast_add`
`eq_top_iff_forall_le` 📖	mathematical	—	`Top.top` `PartENat` `instTop` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`eq_top_iff_forall_lt` `LT.lt.le` `lt_of_lt_of_le` `coe_lt_coe`
`eq_top_iff_forall_lt` 📖	mathematical	—	`Top.top` `PartENat` `instTop` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`natCast_lt_top` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `ne_top_iff` `irrefl` `instIrreflLt`
`eq_zero_iff` 📖	mathematical	—	`PartENat` `instZero` `instLE`	—	`eq_bot_iff`
`find_dom` 📖	mathematical	—	`Part.Dom` `find`	—	—
`find_eq_top_iff` 📖	mathematical	—	`find` `Top.top` `PartENat` `instTop`	—	`eq_top_iff_forall_lt` `lt_find_iff` `le_rfl` `lt_find`
`find_get` 📖	mathematical	`Part.Dom` `find`	`Part.get` `Nat.find`	—	—
`find_le` 📖	mathematical	—	`PartENat` `instLE` `find` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`le_coe_iff` `Nat.find_min'`
`get_add` 📖	mathematical	`Part.Dom` `PartENat` `instAdd`	`Part.get`	—	—
`get_eq_iff_eq_coe` 📖	mathematical	`Part.Dom`	`Part.get` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`get_eq_iff_eq_some`
`get_eq_iff_eq_some` 📖	mathematical	`Part.Dom`	`Part.get` `some`	—	`Part.get_eq_iff_eq_some`
`get_le_get` 📖	mathematical	`Part.Dom`	`Part.get` `PartENat` `instLE`	—	`coe_le_coe` `natCast_get`
`get_natCast` 📖	mathematical	—	`Part.get` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `dom_natCast`	—	`get_natCast'` `dom_natCast`
`get_natCast'` 📖	mathematical	`Part.Dom` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	`Part.get`	—	`natCast_get`
`get_ofNat'` 📖	mathematical	`Part.Dom`	`Part.get`	—	`get_natCast'`
`get_one` 📖	mathematical	`Part.Dom` `PartENat` `instOne`	`Part.get`	—	—
`get_zero` 📖	mathematical	`Part.Dom` `PartENat` `instZero`	`Part.get`	—	—
`instCanLiftNatCastDom` 📖	mathematical	—	`CanLift` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Part.Dom`	—	`Part.some_get`
`instCanonicallyOrderedAdd` 📖	mathematical	—	`CanonicallyOrderedAdd` `PartENat` `instAdd` `instLE`	—	`add_top` `LT.lt.not_ge` `natCast_lt_top` `Nat.cast_add` `add_comm` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `coe_le_coe` `LE.le.trans_eq` `le_top` `top_add` `Eq.ge` `le_add_self` `le_self_add`
`instCharZero` 📖	mathematical	—	`CharZero` `PartENat` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`Part.some_injective`
`instWellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`lt_wf`
`instZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `PartENat` `instZero` `instOne` `instLE`	—	`bot_le`
`isOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `PartENat` `addCommMonoid` `partialOrder`	—	`add_top` `dom_natCast` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`isTotal` 📖	mathematical	—	`IsTotal` `PartENat` `instLE`	—	`le_top` `le_total` `coe_le_coe`
`le_coe_iff` 📖	mathematical	—	`PartENat` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Part.get`	—	`get_natCast'`
`le_def` 📖	mathematical	—	`PartENat` `instLE` `Part.get`	—	—
`le_of_lt_add_one` 📖	mathematical	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instAdd` `instOne`	`instLE`	—	`le_top` `ne_top_iff` `ne_top_of_lt` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero` `Nat.cast_one`
`lt_add_iff_pos_right` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instAdd` `instZero`	—	`add_lt_add_iff_left` `add_zero`
`lt_add_one` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instAdd` `instOne`	—	`lt_add_iff_pos_right` `Nat.cast_zero` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero`
`lt_add_one_iff_lt` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instAdd` `instOne` `instLE`	—	`le_of_lt_add_one` `ne_top_iff` `top_add` `natCast_lt_top` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero`
`lt_coe_iff` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Part.get`	—	`get_natCast'`
`lt_coe_succ_iff_le` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `instLE`	—	`Nat.cast_add` `Nat.cast_one` `lt_add_one_iff_lt`
`lt_def` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Part.get`	—	`lt_iff_le_not_ge` `le_def` `LT.lt.le` `not_lt_of_ge`
`lt_find` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `find`	—	`coe_lt_iff` `find_get` `Nat.find_spec` `Mathlib.Tactic.Contrapose.contrapose₁`
`lt_find_iff` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `find`	—	`Nat.find_min` `lt_of_le_of_lt` `coe_lt_iff` `lt_find`
`lt_wf` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	`wellFounded_lt`
`natCast_get` 📖	mathematical	`Part.Dom`	`PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Part.get`	—	`Part.ext'`
`natCast_inj` 📖	mathematical	—	`PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`instCharZero`
`natCast_lt_top` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `Top.top` `instTop`	—	`Ne.lt_top`
`natCast_ne_top` 📖	—	—	—	—	`ne_of_lt` `natCast_lt_top`
`ne_top_iff` 📖	mathematical	—	`PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`Part.ne_none_iff`
`ne_top_iff_dom` 📖	mathematical	—	`Part.Dom`	—	`not_iff_comm` `Part.eq_none_iff'`
`ne_top_of_lt` 📖	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder`	—	—	`ne_of_lt` `lt_of_lt_of_le` `le_top`
`ne_zero_iff` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Bot.bot` `instBot`	—	`bot_lt_iff_ne_bot`
`not_dom_iff_eq_top` 📖	mathematical	—	`Part.Dom` `Top.top` `PartENat` `instTop`	—	`Iff.not_left` `ne_top_iff_dom`
`not_isMax_natCast` 📖	mathematical	—	`IsMax` `PartENat` `instLE` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	`not_isMax_of_lt` `natCast_lt_top`
`ofENat_coe` 📖	mathematical	—	`ofENat` `ENat` `ENat.instNatCast` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`ofENat_le` 📖	mathematical	—	`PartENat` `instLE` `ofENat` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`toWithTop_le` `toWithTop_ofENat`
`ofENat_lt` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `ofENat` `ENat` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	`toWithTop_lt` `toWithTop_ofENat`
`ofENat_ofNat` 📖	mathematical	—	`ofENat` `PartENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`ofENat_one` 📖	mathematical	—	`ofENat` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `PartENat` `instOne`	—	—
`ofENat_toWithTop` 📖	mathematical	—	`ofENat` `toWithTop`	—	`toWithTop_top'` `toWithTop_natCast'`
`ofENat_top` 📖	mathematical	—	`ofENat` `Top.top` `ENat` `instTopENat` `PartENat` `instTop`	—	—
`ofENat_zero` 📖	mathematical	—	`ofENat` `ENat` `instZeroENat` `PartENat` `instZero`	—	—
`ofNat_lt_top` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `Top.top` `instTop`	—	`natCast_lt_top`
`ofNat_ne_top` 📖	—	—	—	—	`natCast_ne_top`
`one_lt_top` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instOne` `Top.top` `instTop`	—	`natCast_lt_top`
`one_ne_top` 📖	—	—	—	—	`natCast_ne_top`
`pos_iff_one_le` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `instLE` `instOne`	—	`Nat.cast_zero` `Nat.cast_one` `coe_lt_coe` `coe_le_coe`
`some_eq_natCast` 📖	mathematical	—	`some` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`toWithTop_add` 📖	mathematical	—	`toWithTop` `PartENat` `instAdd` `Part.Dom` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`toWithTop.congr_simp` `add_top` `toWithTop_top'` `add_top` `toWithTop_natCast'` `top_add` `top_add`
`toWithTop_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `toWithTop` `PartENat` `instLE`	—	`toWithTop_top'` `toWithTop_natCast'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `isOrderedAddMonoid` `instZeroLEOneClass` `instCharZero`
`toWithTop_lt` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `toWithTop` `PartENat` `partialOrder`	—	`lt_iff_lt_of_le_iff_le` `toWithTop_le`
`toWithTop_natCast` 📖	mathematical	—	`toWithTop` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `ENat` `ENat.instNatCast`	—	—
`toWithTop_natCast'` 📖	mathematical	—	`toWithTop` `PartENat` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `ENat` `ENat.instNatCast`	—	`toWithTop_natCast`
`toWithTop_ofENat` 📖	mathematical	—	`toWithTop` `ofENat`	—	`toWithTop_top'` `toWithTop_natCast'`
`toWithTop_ofNat` 📖	mathematical	—	`toWithTop` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`toWithTop_natCast'`
`toWithTop_one` 📖	mathematical	—	`toWithTop` `PartENat` `instOne` `Part.someDecidable` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	—
`toWithTop_one'` 📖	mathematical	—	`toWithTop` `PartENat` `instOne` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonDecidable` `toWithTop_one`
`toWithTop_some` 📖	mathematical	—	`toWithTop` `some` `instDecidableDomNatSome` `ENat` `ENat.instNatCast`	—	—
`toWithTop_top` 📖	mathematical	—	`toWithTop` `Top.top` `PartENat` `instTop` `Part.noneDecidable` `ENat` `instTopENat`	—	—
`toWithTop_top'` 📖	mathematical	—	`toWithTop` `Top.top` `PartENat` `instTop` `ENat` `instTopENat`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonDecidable` `toWithTop_top`
`toWithTop_zero` 📖	mathematical	—	`toWithTop` `PartENat` `instZero` `Part.someDecidable` `ENat` `instZeroENat`	—	—
`toWithTop_zero'` 📖	mathematical	—	`toWithTop` `PartENat` `instZero` `ENat` `instZeroENat`	—	`Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonDecidable` `toWithTop_zero`
`top_add` 📖	mathematical	—	`PartENat` `instAdd` `Top.top` `instTop`	—	`Part.ext'`
`top_eq_none` 📖	mathematical	—	`Top.top` `PartENat` `instTop` `Part.none`	—	—
`withTopEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `PartENat` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `toWithTop` `Part.Dom`	—	—
`withTopEquiv_le` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `DFunLike.coe` `Equiv` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `instLE`	—	—
`withTopEquiv_lt` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `DFunLike.coe` `Equiv` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `partialOrder`	—	—
`withTopEquiv_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `PartENat` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne` `ENat.instNatCast`	—	`toWithTop_natCast'`
`withTopEquiv_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `PartENat` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `instOfNatAtLeastTwo` `ENat.instNatCast`	—	`toWithTop_ofNat`
`withTopEquiv_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `PartENat` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`toWithTop_one'`
`withTopEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ENat` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `ofENat`	—	—
`withTopEquiv_symm_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ENat` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `ENat.instNatCast` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`withTopEquiv_symm_le` 📖	mathematical	—	`PartENat` `instLE` `DFunLike.coe` `Equiv` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	—
`withTopEquiv_symm_lt` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `DFunLike.coe` `Equiv` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat`	—	—
`withTopEquiv_symm_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ENat` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOne`	—	—
`withTopEquiv_symm_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ENat` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `instOne`	—	—
`withTopEquiv_symm_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ENat` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `Top.top` `instTopENat` `instTop`	—	—
`withTopEquiv_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ENat` `PartENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `withTopEquiv` `instZeroENat` `instZero`	—	—
`withTopEquiv_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `PartENat` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `Top.top` `instTop` `instTopENat`	—	`toWithTop_top'`
`withTopEquiv_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `PartENat` `ENat` `EquivLike.toFunLike` `Equiv.instEquivLike` `withTopEquiv` `instZero` `instZeroENat`	—	`toWithTop_zero'`
`zero_lt_top` 📖	mathematical	—	`PartENat` `Preorder.toLT` `PartialOrder.toPreorder` `partialOrder` `instZero` `Top.top` `instTop`	—	`natCast_lt_top`
`zero_ne_top` 📖	—	—	—	—	`natCast_ne_top`

(root)

Definitions

Name	Category	Theorems
`PartENat` 📖	CompOp	89 math math: `PartENat.top_add`, `PartENat.dom_one`, `PartENat.ofENat_le`, `PartENat.withTopEquiv_symm_apply`, `PartENat.ofENat_one`, `PartENat.instCanonicallyOrderedAdd`, `PartENat.eq_zero_iff`, `PartENat.toWithTop_natCast`, `PartENat.withTopEquiv_one`, `PartENat.lt_find_iff`, `PartENat.coe_lt_coe`, `PartENat.lt_coe_iff`, `PartENat.pos_iff_one_le`, `PartENat.add_one_le_iff_lt`, `PartENat.ofNat_lt_top`, `PartENat.get_natCast`, `PartENat.top_eq_none`, `PartENat.le_coe_iff`, `PartENat.instWellFoundedLT`, `PartENat.toWithTop_lt`, `PartENat.lt_add_one_iff_lt`, `PartENat.not_isMax_natCast`, `PartENat.get_le_get`, `PartENat.toWithTop_zero'`, `PartENat.withTopEquiv_ofNat`, `PartENat.lt_def`, `PartENat.not_dom_iff_eq_top`, `PartENat.add_top`, `PartENat.toWithTop_add`, `PartENat.toWithTop_le`, `PartENat.one_lt_top`, `PartENat.withTopEquiv_symm_ofNat`, `PartENat.ofENat_ofNat`, `PartENat.instCanLiftNatCastDom`, `PartENat.toWithTop_one`, `PartENat.natCast_get`, `PartENat.dom_natCast`, `PartENat.isOrderedAddMonoid`, `PartENat.find_eq_top_iff`, `PartENat.add_right_cancel_iff`, `PartENat.find_le`, `PartENat.ne_zero_iff`, `PartENat.toWithTop_natCast'`, `PartENat.eq_top_iff_forall_le`, `PartENat.natCast_lt_top`, `PartENat.withTopEquiv_symm_one`, `PartENat.le_def`, `PartENat.withTopEquiv_natCast`, `PartENat.coe_le_coe`, `PartENat.instZeroLEOneClass`, `PartENat.eq_top_iff_forall_lt`, `PartENat.coe_succ_le_iff`, `PartENat.coe_lt_iff`, `PartENat.get_eq_iff_eq_coe`, `PartENat.toWithTop_top`, `PartENat.withTopEquiv_top`, `PartENat.toWithTop_top'`, `PartENat.add_lt_add_iff_right`, `PartENat.toWithTop_zero`, `PartENat.ofENat_lt`, `PartENat.withTopEquiv_le`, `PartENat.add_eq_top_iff`, `PartENat.dom_zero`, `PartENat.withTopEquiv_lt`, `PartENat.withTopEquiv_apply`, `PartENat.ofENat_coe`, `PartENat.isTotal`, `PartENat.lt_add_iff_pos_right`, `PartENat.withTopEquiv_symm_zero`, `PartENat.toWithTop_one'`, `PartENat.lt_wf`, `PartENat.add_lt_add_iff_left`, `PartENat.zero_lt_top`, `PartENat.ne_top_iff`, `PartENat.withTopEquiv_zero`, `PartENat.lt_add_one`, `PartENat.withTopEquiv_symm_le`, `PartENat.some_eq_natCast`, `PartENat.coe_le_iff`, `PartENat.ofENat_zero`, `PartENat.withTopEquiv_symm_coe`, `PartENat.lt_find`, `PartENat.ofENat_top`, `PartENat.natCast_inj`, `PartENat.lt_coe_succ_iff_le`, `PartENat.instCharZero`, `PartENat.withTopEquiv_symm_lt`, `PartENat.withTopEquiv_symm_top`, `PartENat.add_left_cancel_iff`

---

← Back to Index