Theorems · Theorem · order theory
Fin.strictMono_natAdd
∀ {m : ℕ} (n : ℕ), StrictMono (Fin.natAdd n)- Defined in
- Mathlib.Order.Fin.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- StrictMonostatement · cited by 706
Cited by12
Results whose statement or proof uses this declaration.
- Fin.natAddOrderEmbproof · cited by 3
- Fin.image_natAdd_uIccproof · cited by 2
- Fin.natAdd_lt_natAdd_iffproof · cited by 1
- Fin.image_natAdd_uIocproof · cited by 0
- Fin.image_natAdd_uIooproof · cited by 0
- Fin.preimage_natAdd_uIcc_natAddproof · cited by 0
- Fin.preimage_natAdd_uIoc_natAddproof · cited by 0
- Fin.natAdd_injproof · cited by 0
- Fin.natAdd_injectiveproof · cited by 0
- Fin.preimage_natAdd_uIoo_natAddproof · cited by 0
- Fin.natAdd_le_natAdd_iffproof · cited by 0
- Fin.natAddOrderEmb_toEmbeddingstatement · cited by 0