Theorems · Theorem · order theory
Disjoint.symm
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] ⦃a b : α⦄, Disjoint a b → Disjoint b a- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 125 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 12 definitions · 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
- Disjointstatement · cited by 2,201
- OrderBotstatement and proof · cited by 1,055
- disjoint_commproof · cited by 49
Cited by125
Results whose statement or proof uses this declaration.
- IsCompl.symmproof · cited by 80
- disjoint_compl_rightproof · cited by 47
- Metric.closedBall_sdiff_ballproof · cited by 10
- not_tendsto_nhds_of_tendsto_atTopproof · cited by 7
- Finset.disjoint_sdiffproof · cited by 7
- Disjoint.sdiff_eq_rightproof · cited by 6
- regularSpace_TFAEproof · cited by 6
- SeparatedNhds.symmproof · cited by 6
- MonotoneOn.countable_setOfPred_two_preimagesproof · cited by 5
- cauchySeq_finset_iff_sum_vanishingproof · cited by 5
- exists_continuous_one_zero_of_isCompactproof · cited by 5
- ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMemproof · cited by 5