Theorems · Theorem · order theory
iSup_bool_eq
∀ {α : Type u_1} [inst : CompleteLattice α] {f : Bool → α}, ⨆ b, f b = f true ⊔ f false- Defined in
- Mathlib.Order.CompleteLattice.Lemmas
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- iSupstatement · cited by 2,415
- CompleteLatticestatement and proof · cited by 1,048
- SupSet.sSupproof · cited by 954
- sup_commproof · cited by 165
- sSup_pairproof · cited by 11
- Bool.range_eqproof · cited by 2
Cited by12
Results whose statement or proof uses this declaration.
- sup_eq_iSupproof · cited by 7
- Filter.comap_supproof · cited by 5
- Finsupp.supported_unionproof · cited by 2
- MeasureTheory.ae_restrict_union_eqproof · cited by 2
- MeasureTheory.OuterMeasure.sup_applyproof · cited by 2
- AlgebraicGeometry.nonempty_isColimit_binaryCofanMk_of_isComplproof · cited by 1
- IsSemisimpleModule.supproof · cited by 0
- CompletelyDistribLattice.MinimalAxioms.toCompleteDistribLatticeproof · cited by 0
- dimH_unionproof · cited by 0
- rel_sup_addproof · cited by 0
- rel_sup_mulproof · cited by 0
- Submodule.isHilbertSumOrthogonalproof · cited by 0