Mathlib Map

Theorems · Theorem · order theory

Disjoint.ne

∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, a ≠ ⊥ → Disjoint a b → a ≠ b
Defined in
Mathlib.Order.Disjoint
Cited by
5 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
PartialOrderOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion · cited by 1IsSetSemiring.pairwiseDis…BoxIntegral.Box.ne_of_disjoint_coe · cited by 1Box.ne_of_disjoint_coeBoxIntegral.Box.splitLower_ne_splitUpper · cited by 1Box.splitLower_ne_splitUp…BoxIntegral.Box.injective_splitCenterBox · cited by 0Box.injective_splitCenter…Topology.RelCWComplex.openCell_congr · cited by 0RelCWComplex.openCell_con…PartialOrder · cited by 6410PartialOrderBot.bot · cited by 4720Bot.botDisjoint · cited by 2201DisjointOrderBot · cited by 1055OrderBotdisjoint_self · cited by 28disjoint_selfDisjoint.neCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by5

Results whose statement or proof uses this declaration.