Mathlib Map

Theorems · Theorem · order theory

Set.finite_le_nat

∀ (n : ℕ), {i | i ≤ n}.Finite
Defined in
Mathlib.Data.Set.Finite.Basic
Cited by
16 results in Mathlib
Foundations
Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.measure_spanningSets_lt_top · cited by 25MeasureTheory.measure_spa…Nat.sSup_mem · cited by 5Nat.sSup_memrefinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set · cited by 3refinement_of_locallyComp…SequentiallyComplete.setSeq_mem · cited by 2SequentiallyComplete.setS…isCompact_accumulate · cited by 2isCompact_accumulateFilter.high_scores · cited by 2Filter.high_scoresIrrational.eventually_forall_le_dist_cast_div_of_denom_le · cited by 1Irrational.eventually_for…closure_iUnion₂_le_nat · cited by 1closure_iUnion₂_le_natIsSeqCompact.isComplete · cited by 1IsSeqCompact.isCompleteSimpleGraph.Walk.exists_isPath_forall_isPath_length_le_length · cited by 1Walk.exists_isPath_forall…CauchySeq.totallyBounded_range · cited by 1CauchySeq.totallyBounded_…isLindelof_accumulate · cited by 0isLindelof_accumulateSet.finite_range_findGreatest · cited by 0Set.finite_range_findGrea…SimpleGraph.Walk.exists_isTrail_forall_isTrail_length_le_length · cited by 0Walk.exists_isTrail_foral…interior_iInter₂_le_nat · cited by 0interior_iInter₂_le_natSet.ofPred · cited by 6101Set.ofPredSet.Finite · cited by 1814Set.FiniteSet.toFinite · cited by 174Set.toFiniteSet.finite_le_natCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by16

Results whose statement or proof uses this declaration.