Nth

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

Statistics

Metric	Count
Definitions giCountNth, nth	2
Theorems count_eq_zero, count_le_iff_le_nth, count_nth, count_nth_of_infinite, count_nth_of_lt_card_finite, count_nth_succ, count_nth_succ_of_infinite, count_nth_zero, eq_nth_of_strictMonoOn_of_mapsTo_of_surjOn, exists_lt_card_finite_nth_eq, exists_lt_card_nth_eq, filter_range_nth_eq_insert, filter_range_nth_eq_insert_of_finite, filter_range_nth_eq_insert_of_infinite, filter_range_nth_subset_insert, gc_count_nth, image_nth_Iio_card, isLeast_nth, isLeast_nth_of_infinite, isLeast_nth_of_lt_card, le_nth, le_nth_count, le_nth_count', le_nth_of_count_le, le_nth_of_lt_nth_succ, le_nth_of_monotoneOn_of_surjOn, le_of_nth_le_nth_of_lt_card, lt_card_toFinset_of_nth_ne_zero, lt_nth_iff_count_lt, lt_of_nth_lt_nth_of_lt_card, nth_add, nth_add_eq_sub, nth_add_one, nth_add_one_eq_sub, nth_apply_eq_orderIsoOfNat, nth_comp_of_strictMono, nth_count, nth_count_eq_sInf, nth_eq_getD_sort, nth_eq_orderEmbOfFin, nth_eq_orderIsoOfNat, nth_eq_sInf, nth_eq_zero, nth_eq_zero_mono, nth_false, nth_injOn, nth_injective, nth_le_nth, nth_le_nth', nth_le_nth_of_lt_card, nth_le_of_strictMonoOn_of_mapsTo, nth_lt_nth, nth_lt_nth', nth_lt_nth_of_lt_card, nth_lt_of_lt_count, nth_mem, nth_mem_anti, nth_mem_of_infinite, nth_mem_of_lt_card, nth_mem_of_ne_zero, nth_monotone, nth_ne_zero_anti, nth_of_card_le, nth_of_forall, nth_of_forall_not, nth_strictMono, nth_strictMonoOn, nth_true, nth_zero, nth_zero_of_exists, nth_zero_of_zero, range_nth_of_finite, range_nth_of_infinite, range_nth_subset, subset_range_nth, surjective_count_of_infinite_setOf	76
Total	78

Nat

Definitions

Name	Category	Theorems
giCountNth 📖	CompOp	—
nth 📖	CompOp	75 math math: nth_zero_of_zero, nth_of_forall_not, nth_eq_zero, filter_range_nth_subset_insert, nth_monotone, nth_injective, nth_strictMono, filter_range_nth_eq_insert_of_finite, le_nth_count, nth_of_card_le, nth_mem, nth_zero, count_nth_of_lt_card_finite, nth_prime_four_eq_eleven, nth_le_of_strictMonoOn_of_mapsTo, exists_lt_card_finite_nth_eq, count_le_iff_le_nth, count_nth_succ_of_infinite, nth_prime_three_eq_seven, nth_le_nth_of_lt_card, nth_add_one_eq_sub, isLeast_nth, gc_count_nth, nth_le_nth', isLeast_nth_of_infinite, nth_true, nth_eq_sInf, nth_zero_of_exists, nth_lt_nth', exists_lt_card_nth_eq, nth_lt_nth, nth_apply_eq_orderIsoOfNat, nth_injOn, nth_mem_of_lt_card, nth_mem_of_infinite, range_nth_subset, nth_mem_of_ne_zero, count_nth, nth_strictMonoOn, prime_nth_prime, le_nth_count', count_nth_of_infinite, primeCounting'_nth_eq, add_two_le_nth_prime, nth_add_one, nth_eq_orderEmbOfFin, nth_prime_zero_eq_two, nth_false, nth_eq_getD_sort, nth_prime_one_eq_three, le_nth, count_nth_succ, nth_le_nth, range_nth_of_finite, nth_count, lt_nth_iff_count_lt, eq_nth_of_strictMonoOn_of_mapsTo_of_surjOn, range_nth_of_infinite, nth_prime_two_eq_five, nth_lt_nth_of_lt_card, count_eq_zero, nth_eq_orderIsoOfNat, filter_range_nth_eq_insert_of_infinite, nth_count_eq_sInf, isLeast_nth_of_lt_card, nth_comp_of_strictMono, nth_lt_of_lt_count, nth_add_eq_sub, nth_add, filter_range_nth_eq_insert, nth_of_forall, subset_range_nth, count_nth_zero, image_nth_Iio_card, le_nth_of_monotoneOn_of_surjOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
count_eq_zero 📖	mathematical	—	count nth	—	nth_zero_of_exists le_find_iff count_iff_forall_not
count_le_iff_le_nth 📖	mathematical	Set.Infinite setOf	count nth	—	gc_count_nth
count_nth 📖	mathematical	Finset.card Set.Finite.toFinset setOf	count nth	—	count_nth_zero count_eq_card_filter_range filter_range_nth_eq_insert Finset.card_insert_of_notMem
count_nth_of_infinite 📖	mathematical	Set.Infinite setOf	count nth	—	count_nth
count_nth_of_lt_card_finite 📖	mathematical	Finset.card Set.Finite.toFinset setOf	count nth	—	count_nth
count_nth_succ 📖	mathematical	Finset.card Set.Finite.toFinset setOf	count nth	—	count_succ count_nth nth_mem
count_nth_succ_of_infinite 📖	mathematical	Set.Infinite setOf	count nth	—	count_succ count_nth_of_infinite nth_mem_of_infinite
count_nth_zero 📖	mathematical	—	count nth	—	count_eq_card_filter_range Finset.card_eq_zero Finset.filter_eq_empty_iff nth_zero LT.lt.not_ge Finset.mem_range sInf_le
eq_nth_of_strictMonoOn_of_mapsTo_of_surjOn 📖	mathematical	Set.SurjOn setOf Set.MapsTo StrictMonoOn instPreorder	Set.EqOn nth	—	le_antisymm le_nth_of_monotoneOn_of_surjOn StrictMonoOn.monotoneOn nth_le_of_strictMonoOn_of_mapsTo
exists_lt_card_finite_nth_eq 📖	mathematical	—	Finset.card Set.Finite.toFinset setOf nth	—	image_nth_Iio_card Set.mem_setOf_eq
exists_lt_card_nth_eq 📖	mathematical	—	Finset.card Set.Finite.toFinset setOf nth	—	Set.finite_or_infinite exists_lt_card_finite_nth_eq range_nth_of_infinite Set.mem_setOf_eq
filter_range_nth_eq_insert 📖	mathematical	Finset.card Set.Finite.toFinset setOf	Finset.filter Finset.range nth Finset Finset.instInsert	—	HasSubset.Subset.antisymm Finset.instAntisymmSubset filter_range_nth_subset_insert nth_lt_nth' nth_mem LT.lt.trans
filter_range_nth_eq_insert_of_finite 📖	mathematical	Finset.card Set.Finite.toFinset setOf	Finset.filter Finset.range nth Finset Finset.instInsert	—	filter_range_nth_eq_insert
filter_range_nth_eq_insert_of_infinite 📖	mathematical	Set.Infinite setOf	Finset.filter Finset.range nth Finset Finset.instInsert	—	filter_range_nth_eq_insert
filter_range_nth_subset_insert 📖	mathematical	—	Finset Finset.instHasSubset Finset.filter Finset.range nth Finset.instInsert	—	LE.le.eq_or_lt le_nth_of_lt_nth_succ
gc_count_nth 📖	mathematical	Set.Infinite setOf	GaloisConnection instPreorder count nth	—	GaloisInsertion.gc
image_nth_Iio_card 📖	mathematical	—	Set.image nth Set.Iio instPreorder Finset.card Set.Finite.toFinset setOf	—	Set.ext nth_eq_orderEmbOfFin Finset.range_orderEmbOfFin Set.Finite.coe_toFinset
isLeast_nth 📖	mathematical	Finset.card Set.Finite.toFinset setOf	IsLeast nth	—	nth_mem nth_lt_nth' exists_lt_card_nth_eq lt_or_ge LT.lt.ne nth_le_nth'
isLeast_nth_of_infinite 📖	mathematical	Set.Infinite setOf	IsLeast nth	—	isLeast_nth
isLeast_nth_of_lt_card 📖	mathematical	Finset.card Set.Finite.toFinset setOf	IsLeast nth	—	isLeast_nth
le_nth 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	Set.finite_or_infinite StrictMonoOn.Iic_id_le instIsSuccArchimedean StrictMonoOn.mono nth_strictMonoOn Set.Iic_subset_Iio le_rfl StrictMono.id_le instWellFoundedLTNat nth_strictMono
le_nth_count 📖	mathematical	Set.Infinite setOf	nth count	—	Set.Infinite.exists_gt le_nth_count' LT.lt.le
le_nth_count' 📖	mathematical	—	nth count	—	LE.le.trans le_csInf Eq.ge nth_count_eq_sInf
le_nth_of_count_le 📖	mathematical	nth	count	—	not_lt LE.le.not_gt nth_lt_of_lt_count
le_nth_of_lt_nth_succ 📖	—	nth	—	—	Set.finite_or_infinite exists_lt_card_finite_nth_eq lt_or_ge StrictMonoOn.le_iff_le nth_strictMonoOn LT.lt.trans StrictMonoOn.lt_iff_lt nth_of_card_le LE.le.not_gt subset_range_nth nth_le_nth nth_lt_nth
le_nth_of_monotoneOn_of_surjOn 📖	mathematical	Set.SurjOn setOf MonotoneOn instPreorder Finset.card Set.Finite.toFinset	nth	—	nth_zero le_csInf nth_mem nth_eq_sInf nth_lt_nth' MonotoneOn.reflect_lt
le_of_nth_le_nth_of_lt_card 📖	—	nth Finset.card Set.Finite.toFinset setOf	—	—	not_lt LE.le.not_gt nth_lt_nth_of_lt_card
lt_card_toFinset_of_nth_ne_zero 📖	mathematical	—	Finset.card Set.Finite.toFinset setOf	—	—
lt_nth_iff_count_lt 📖	mathematical	Set.Infinite setOf	count nth	—	GaloisConnection.lt_iff_lt gc_count_nth
lt_of_nth_lt_nth_of_lt_card 📖	—	nth Finset.card Set.Finite.toFinset setOf	—	—	not_le LT.lt.not_ge nth_le_nth_of_lt_card
nth_add 📖	mathematical	—	nth	—	nth_comp_of_strictMono StrictMono.add_const IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid strictMono_id not_le le_iff_exists_add' instCanonicallyOrderedAdd lt_card_toFinset_of_nth_ne_zero
nth_add_eq_sub 📖	mathematical	—	nth	—	nth_add
nth_add_one 📖	mathematical	—	nth	—	nth_add
nth_add_one_eq_sub 📖	mathematical	—	nth	—	nth_add_eq_sub
nth_apply_eq_orderIsoOfNat 📖	mathematical	Set.Infinite setOf	nth Set Set.instMembership DFunLike.coe OrderIso Set.Elem instFunLikeOrderIso Subtype.orderIsoOfNat Set.Infinite.to_subtype	—	Set.Infinite.to_subtype instIsTransLe LE.total nth.eq_1
nth_comp_of_strictMono 📖	mathematical	StrictMono instPreorder Set Set.instMembership Set.range Finset.card Set.Finite.toFinset setOf	nth	—	Set.ext case_strong_induction_on nth_zero nth_mem Monotone.map_csInf instWellFoundedLTNat StrictMono.monotone Set.mem_setOf_eq nth_eq_sInf nth_lt_nth' StrictMono.lt_iff_lt LT.lt.trans
nth_count 📖	mathematical	—	nth count	—	count_lt_card count_injective nth_mem count_nth
nth_count_eq_sInf 📖	mathematical	—	nth count InfSet.sInf instInfSet setOf	—	nth_eq_sInf Set.ext not_lt count_strict_mono lt_self_iff_false nth_count lt_of_lt_of_le nth_lt_of_lt_count
nth_eq_getD_sort 📖	mathematical	—	nth Finset.sort Set.Finite.toFinset setOf instIsTransLe instPreorder LE.total instLinearOrder	—	instIsTransLe LE.total
nth_eq_orderEmbOfFin 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instFunLikeOrderEmbedding Finset.orderEmbOfFin	—	instIsTransLe LE.total nth_eq_getD_sort instAntisymmLe Finset.orderEmbOfFin_apply List.getD_eq_getElem
nth_eq_orderIsoOfNat 📖	mathematical	Set.Infinite setOf	nth Set.Elem Set Set.instMembership DFunLike.coe OrderIso instFunLikeOrderIso Subtype.orderIsoOfNat Set.Infinite.to_subtype	—	Set.Infinite.to_subtype nth_apply_eq_orderIsoOfNat
nth_eq_sInf 📖	mathematical	—	nth InfSet.sInf instInfSet setOf	—	IsLeast.csInf_eq isLeast_nth Mathlib.Tactic.Push.not_forall_eq nth_of_card_le Set.eq_empty_of_forall_notMem exists_lt_card_nth_eq LT.lt.false LT.lt.trans_le sInf_empty
nth_eq_zero 📖	mathematical	—	nth Finset.card Set.Finite.toFinset setOf	—	nth_mem nonpos_iff_eq_zero instCanonicallyOrderedAdd le_nth nth_zero_of_zero nth_of_card_le
nth_eq_zero_mono 📖	—	nth	—	—	LE.le.trans
nth_false 📖	mathematical	—	nth	—	nth_of_forall_not
nth_injOn 📖	mathematical	—	Set.InjOn nth Set.Iio instPreorder Finset.card Set.Finite.toFinset setOf	—	StrictMonoOn.injOn nth_strictMonoOn
nth_injective 📖	mathematical	Set.Infinite setOf	nth	—	StrictMono.injective nth_strictMono
nth_le_nth 📖	mathematical	Set.Infinite setOf	nth	—	StrictMono.le_iff_le nth_strictMono
nth_le_nth' 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	Set.finite_or_infinite nth_le_nth_of_lt_card nth_le_nth
nth_le_nth_of_lt_card 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	StrictMonoOn.monotoneOn nth_strictMonoOn LE.le.trans_lt
nth_le_of_strictMonoOn_of_mapsTo 📖	mathematical	Set.MapsTo setOf StrictMonoOn instPreorder	nth	—	strong_induction_on nth_eq_sInf csInf_le Mathlib.Tactic.Push.not_forall_eq instIsTransLe LE.total nth.eq_1 List.getD_eq_default Finset.length_sort
nth_lt_nth 📖	mathematical	Set.Infinite setOf	nth	—	StrictMono.lt_iff_lt nth_strictMono
nth_lt_nth' 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	Set.finite_or_infinite nth_lt_nth_of_lt_card nth_lt_nth
nth_lt_nth_of_lt_card 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	nth_strictMonoOn LT.lt.trans
nth_lt_of_lt_count 📖	mathematical	count	nth	—	Monotone.reflect_lt count_monotone count_nth LT.lt.trans_le count_le_card
nth_mem 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	Set.finite_or_infinite nth_mem_of_lt_card nth_mem_of_infinite
nth_mem_anti 📖	—	nth	—	—	nth_mem LE.le.trans
nth_mem_of_infinite 📖	mathematical	Set.Infinite setOf	nth	—	Set.range_subset_iff Eq.le range_nth_of_infinite
nth_mem_of_lt_card 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	Eq.subset Set.instReflSubset image_nth_Iio_card Set.mem_image_of_mem
nth_mem_of_ne_zero 📖	mathematical	—	nth	—	nth_mem lt_card_toFinset_of_nth_ne_zero
nth_monotone 📖	mathematical	Set.Infinite setOf	Monotone instPreorder nth	—	StrictMono.monotone nth_strictMono
nth_ne_zero_anti 📖	—	—	—	—	nth_eq_zero_mono
nth_of_card_le 📖	mathematical	Finset.card Set.Finite.toFinset setOf	nth	—	instIsTransLe LE.total nth.eq_1 List.getD_eq_default Finset.length_sort
nth_of_forall 📖	mathematical	—	nth	—	count_of_forall LT.lt.le nth_count le_rfl
nth_of_forall_not 📖	mathematical	—	nth	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Finset.coe_range Set.mem_setOf nth_of_card_le Set.Finite.subset Finset.finite_toSet LE.le.trans_eq Finset.card_le_card Set.Finite.toFinset_subset Finset.card_range
nth_strictMono 📖	mathematical	Set.Infinite setOf	StrictMono instPreorder nth	—	Set.Infinite.to_subtype nth_eq_orderIsoOfNat StrictMono.comp Subtype.strictMono_coe OrderIso.strictMono
nth_strictMonoOn 📖	mathematical	—	StrictMonoOn instPreorder nth Set.Iio Finset.card Set.Finite.toFinset setOf	—	nth_eq_orderEmbOfFin OrderEmbedding.strictMono
nth_true 📖	mathematical	—	nth	—	nth_of_forall
nth_zero 📖	mathematical	—	nth InfSet.sInf instInfSet setOf	—	nth_eq_sInf instCanonicallyOrderedAdd instIsEmptyFalse
nth_zero_of_exists 📖	mathematical	—	nth find	—	nth_zero Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable sInf_def
nth_zero_of_zero 📖	mathematical	—	nth	—	nth_zero
range_nth_of_finite 📖	mathematical	—	Set.range nth Set Set.instInsert setOf	—	instIsTransLe LE.total nth_eq_getD_sort Set.range_list_getD
range_nth_of_infinite 📖	mathematical	Set.Infinite setOf	Set.range nth	—	Set.Infinite.to_subtype nth_eq_orderIsoOfNat Subtype.coe_comp_ofNat_range
range_nth_subset 📖	mathematical	—	Set Set.instHasSubset Set.range nth Set.instInsert setOf	—	Set.finite_or_infinite Eq.subset Set.instReflSubset range_nth_of_finite Eq.trans_subset range_nth_of_infinite Set.subset_insert
subset_range_nth 📖	mathematical	—	Set Set.instHasSubset setOf Set.range nth	—	exists_lt_card_nth_eq
surjective_count_of_infinite_setOf 📖	mathematical	Set.Infinite setOf	count	—	count_nth_of_infinite

---

← Back to Index