Theorems · Theorem · order theory
Set.infinite_univ
∀ {α : Type u} [h : Infinite α], Set.univ.Infinite- Defined in
- Mathlib.Data.Set.Finite.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
- Assumes
- Infinite
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.
- Set.univstatement · cited by 3,945
- Infinitestatement and proof · cited by 352
- Set.Infinitestatement · cited by 263
- Set.infinite_univ_iffproof · cited by 3
Cited by13
Results whose statement or proof uses this declaration.
- Set.infinite_range_of_injectiveproof · cited by 9
- Set.Finite.exists_lt_map_eq_of_forall_memproof · cited by 6
- MvPolynomial.funextproof · cited by 5
- ZLattice.rankproof · cited by 5
- LinearMap.support_singularValuesproof · cited by 3
- NumberField.Embeddings.pow_eq_one_of_norm_le_oneproof · cited by 2
- Set.Finite.infinite_complproof · cited by 2
- Set.infinite_of_finite_complproof · cited by 2
- Set.Infinite.exists_subset_ncard_eqproof · cited by 1
- Set.Finite.exists_notMemproof · cited by 1
- FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zeroproof · cited by 1
- exists_orderEmbedding_covby_of_forall_covby_finite_of_botproof · cited by 1