Theorems · Theorem · order theory
Disjoint.mono_right
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c : α}, b ≤ c → Disjoint a c → Disjoint a b- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 64 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- PartialOrderOrderBot
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.
- PartialOrderstatement and proof · cited by 6,410
- Disjointstatement · cited by 2,201
- le_rflproof · cited by 1,558
- OrderBotstatement and proof · cited by 1,055
- Disjoint.monoproof · cited by 69
Cited by64
Results whose statement or proof uses this declaration.
- Set.disjoint_of_subset_rightproof · cited by 9
- Disjoint.inf_rightproof · cited by 6
- iSupIndep.compproof · cited by 6
- Finset.supIndep_iff_disjoint_eraseproof · cited by 6
- regularSpace_TFAEproof · cited by 6
- le_sdiff_rightproof · cited by 4
- Disjoint.inf_right'proof · cited by 4
- sSupIndep.monoproof · cited by 4
- Finset.SupIndep.biUnionproof · cited by 4
- iSupIndep.disjoint_biSupproof · cited by 4
- Matroid.closure_union_eq_of_subset_coloopsproof · cited by 4
- IsCompact.exists_cthickening_subset_openproof · cited by 4