Theorems · Theorem · order theory
exists_covby_infinite_Ici_of_infinite_Ici
∀ {α : Type u_1} [inst : PartialOrder α] {a : α} [IsStronglyAtomic α],
(Set.Ici a).Infinite → {x | a ⋖ x}.Finite → ∃ b, a ⋖ b ∧ (Set.Ici b).Infinite- Defined in
- Mathlib.Order.Atoms.Finite
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PartialOrderIsStronglyAtomic
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Set.ofPredstatement and proof · cited by 6,101
- Set.Finitestatement and proof · cited by 1,814
- Set.Icistatement and proof · cited by 1,070
- CovBystatement and proof · cited by 290
- Set.Finite.subsetproof · cited by 285
- Set.Infinitestatement and proof · cited by 263
- LE.le.lt_of_neproof · cited by 116
- Set.finite_singletonproof · cited by 70
- Set.mem_biUnionproof · cited by 37
- Set.Finite.biUnionproof · cited by 31
- IsStronglyAtomicstatement and proof · cited by 17
Cited by2
Results whose statement or proof uses this declaration.
- exists_seq_covby_of_forall_covby_finiteproof · cited by 1
- exists_covby_infinite_Iic_of_infinite_Iicproof · cited by 0