Theorems · Theorem · order theory
Order.Ideal.eq_sup_of_le_sup
∀ {P : Type u_1} [inst : DistribLattice P] {I J : Order.Ideal P} {x i j : P},
i ∈ I → j ∈ J → x ≤ i ⊔ j → ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'- Defined in
- Mathlib.Order.Ideal
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
- Assumes
- DistribLattice
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.
- inf_le_rightproof · cited by 238
- DistribLatticestatement and proof · cited by 150
- Order.Idealstatement and proof · cited by 102
- inf_sup_leftproof · cited by 28
- Order.Ideal.lowerproof · cited by 11
- left_eq_infproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- Order.Ideal.coe_sup_eqproof · cited by 0