Theorems · Theorem · order theory
sSupIndep.mono
∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α}, sSupIndep s → ∀ {t : Set α}, t ⊆ s → sSupIndep t- Defined in
- Mathlib.Order.SupIndep
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 58 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.
Cites6
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
- CompleteLatticestatement and proof · cited by 1,048
- Disjoint.mono_rightproof · cited by 64
- sSupIndepstatement and proof · cited by 39
- sSup_le_sSupproof · cited by 24
- Set.sdiff_subset_sdiff_leftproof · cited by 20
Cited by4
Results whose statement or proof uses this declaration.
- WellFoundedGT.finite_of_sSupIndepproof · cited by 2
- sSupIndep_iUnion_of_directedproof · cited by 1
- sSupIndep_iff_finiteproof · cited by 1
- sSupIndep.disjoint_sSupproof · cited by 0