Theorems · Theorem · order theory
Set.Infinite.mono
∀ {α : Type u} {s t : Set α}, s ⊆ t → s.Infinite → t.Infinite- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.Finiteproof · cited by 1,814
- Set.Finite.subsetproof · cited by 285
- Set.Infinitestatement · cited by 263
Cited by25
Results whose statement or proof uses this declaration.
- Set.Icc_infiniteproof · cited by 3
- Filter.cofinite.blimsup_set_eqproof · cited by 3
- Pell.exists_of_not_isSquareproof · cited by 3
- Module.eq_of_mapsTo_reflection_of_memproof · cited by 2
- MonoidHom.map_finprod_of_preimage_oneproof · cited by 2
- Set.infinite_of_injective_forall_memproof · cited by 2
- infinite_not_isOfFinAddOrderproof · cited by 2
- Set.Infinite.image2_leftproof · cited by 1
- Set.Infinite.image2_rightproof · cited by 1
- Polynomial.existsUnique_hilbertPolyproof · cited by 1
- Set.ncard_insert_leproof · cited by 1
- Set.Ioc_infiniteproof · cited by 1