Theorems · Definition · order theory
Set.Infinite.natEmbedding
{α : Type u} → (s : Set α) → s.Infinite → ℕ ↪ ↑sEmbedding of ℕ into an infinite set.
- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.Elemstatement and proof · cited by 7,166
- Function.Embeddingstatement · cited by 988
- Set.Infinitestatement and proof · cited by 263
- Infinite.natEmbeddingproof · cited by 12
Cited by10
Results whose statement or proof uses this declaration.
- Set.VAddAntidiagonal.finite_of_isPWOproof · cited by 16
- IsAntichain.finite_of_partiallyWellOrderedOnproof · cited by 6
- Set.Infinite.exists_subset_card_eqproof · cited by 4
- Set.SMulAntidiagonal.finite_of_isPWOproof · cited by 2
- Set.MulAntidiagonal.finite_of_isPWOproof · cited by 1
- Set.AddAntidiagonal.finite_of_isPWOproof · cited by 1
- IsCountablyCompact.exists_accPt_of_infiniteproof · cited by 1
- IsAntichain.finite_of_wellQuasiOrderedproof · cited by 1
- Set.Infinite.natEmbedding.congr_simpstatement and proof · cited by 0
- Set.Infinite.exists_subset_countable_infiniteproof · cited by 0