Theorems · Theorem · order theory
Disjoint.mono
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
a ≤ b → c ≤ d → Disjoint b d → Disjoint a c- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 69 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- PartialOrderOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- LE.le.transproof · cited by 3,151
- Disjointstatement and proof · cited by 2,201
- OrderBotstatement and proof · cited by 1,055
Cited by69
Results whose statement or proof uses this declaration.
- Disjoint.mono_rightproof · cited by 64
- Disjoint.mono_leftproof · cited by 50
- pairwise_disjoint_monoproof · cited by 10
- Set.disjoint_of_subsetproof · cited by 7
- ProbabilityTheory.Kernel.rnDeriv_add_singularPartproof · cited by 7
- SeparatedNhds.disjoint_closure_leftproof · cited by 4
- Filter.Tendsto.disjointproof · cited by 4
- disjoint_memPartitionproof · cited by 3
- Finset.disjoint_filter_filterproof · cited by 3
- MeasureTheory.VectorMeasure.restrict_le_restrict_iUnionproof · cited by 3
- connectedComponent_eq_iInter_isClopenproof · cited by 2
- MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOnproof · cited by 2