Theorems · Definition · order theory
ChainCompletePartialOrder.bot
{α : Type u_1} → [ChainCompletePartialOrder α] → α → (α → α) → Set αThe bottom admissible set with base point x and inflationary function f
- Defined in
- Mathlib.Order.BourbakiWitt
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- ChainCompletePartialOrder
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.ofPredproof · cited by 6,101
- Set.sInterproof · cited by 225
- ChainCompletePartialOrderstatement and proof · cited by 19
- ChainCompletePartialOrder.IsAdmissibleproof · cited by 8
Cited by14
Results whose statement or proof uses this declaration.
- ChainCompletePartialOrder.bot_isAdmissiblestatement and proof · cited by 4
- ChainCompletePartialOrder.IsExtremePt.mem_botstatement · cited by 3
- ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_ltstatement · cited by 2
- ChainCompletePartialOrder.IsExtremePt.setOfPred_isExtremePt_eq_botstatement · cited by 2
- ChainCompletePartialOrder.IsExtremePt.setOfPred_isExtremePt_isAdmissibleproof · cited by 2
- ChainCompletePartialOrder.map_mem_botstatement and proof · cited by 2
- ChainCompletePartialOrder.subset_bot_iffstatement and proof · cited by 2
- ChainCompletePartialOrder.IsExtremePt.bot_eq_of_le_or_map_lestatement and proof · cited by 2
- ChainCompletePartialOrder.IsExtremePt.mem_bot_iff_isExtremePtstatement · cited by 1
- ChainCompletePartialOrder.IsExtremePt.bot_isChainstatement and proof · cited by 1
- ChainCompletePartialOrder.IsExtremePt.recOnstatement and proof · cited by 0
- ChainCompletePartialOrder.IsExtremePt.setOf_isExtremePt_eq_botstatement · cited by 0