Mathlib Map

Theorems · Theorem · order theory

dite_ne_top

∀ {α : Type u} [inst : Top α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α},
  (∀ (h : p), a h ≠ ⊤) → (∀ (h : ¬p), b h ≠ ⊤) → (if h : p then a h else b h) ≠ ⊤
Defined in
Mathlib.Order.BoundedOrder.Basic
Cited by
2 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
TopDecidable
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.projectiveFamilyContent_ne_top · cited by 3MeasureTheory.projectiveF…ite_ne_top · cited by 0ite_ne_topTop.top · cited by 9680Top.topTop · cited by 93Topdite_ne_topCITED BYCITES

Cites2

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

  • Top.topstatement and proof · cited by 9,680
  • Topstatement and proof · cited by 93

Cited by2

Results whose statement or proof uses this declaration.