Mathlib Map

Theorems · Theorem · order theory

WCovBy.eq_or_eq

∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, a ⩿ b → a ≤ c → c ≤ b → c = a ∨ c = b
Defined in
Mathlib.Order.Cover
Cited by
5 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PartialOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CovBy.eq_or_eq · cited by 2CovBy.eq_or_eqWCovBy.le_and_le_iff · cited by 1WCovBy.le_and_le_iffrange_eq_image_tsupport_or · cited by 0range_eq_image_tsupport_orwcovBy_iff_le_and_eq_or_eq · cited by 0wcovBy_iff_le_and_eq_or_eqrange_eq_image_mulTSupport_or · cited by 0range_eq_image_mulTSuppor…PartialOrder · cited by 6410PartialOrderLE.le.eq_or_lt · cited by 220le.eq_or_ltWCovBy · cited by 107WCovByWCovBy.eq_or_eqCITED BYCITES

Cites3

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.