Theorems · Theorem · order theory
ciSup_of_empty
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] [IsEmpty ι] (f : ι → α), ⨆ i, f i = ⊥- Cited by
- 23 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botstatement and proof · cited by 4,720
- iSupstatement · cited by 2,415
- IsEmptystatement and proof · cited by 759
- ConditionallyCompleteLinearOrderBotstatement and proof · cited by 84
- csSup_emptyproof · cited by 28
- iSup_of_empty'proof · cited by 16
Cited by23
Results whose statement or proof uses this declaration.
- Monotone.measure_iUnionproof · cited by 10
- ProbabilityTheory.Kernel.bound_eq_zero_of_isEmptyproof · cited by 4
- ENNReal.iSup_add_iSupproof · cited by 3
- ENat.mul_iSupproof · cited by 3
- Order.krullDim_eq_iSup_heightproof · cited by 3
- Cardinal.preBeth_zeroproof · cited by 3
- PSet.rank_emptyproof · cited by 2
- ENat.iSup_add_iSupproof · cited by 2
- Cardinal.ciSup_mulproof · cited by 2
- OrderIso.map_ciSup'proof · cited by 1
- Cardinal.iSup_of_emptyproof · cited by 1
- MeasureTheory.lintegral_iSup_directed_of_measurableproof · cited by 1