Mathlib Map

Theorems · Theorem · order theory

iSup_or

∀ {α : Type u_1} [inst : CompleteLattice α] {p q : Prop} {s : p ∨ q → α},
  ⨆ (x : p ∨ q), s x = (⨆ (i : p), s ⋯) ⊔ ⨆ (j : q), s ⋯
Defined in
Mathlib.Order.CompleteLattice.Basic
Cited by
3 results in Mathlib
Foundations
Depth 14 from the axioms · uses no axioms
Assumes
CompleteLattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

iSup_insert · cited by 10iSup_insertiSup_union · cited by 8iSup_unionSet.iUnion_or · cited by 3Set.iUnion_oriSup · cited by 2415iSuple_antisymm · cited by 2068le_antisymmCompleteLattice · cited by 1048CompleteLatticele_iSup · cited by 207le_iSupiSup_le · cited by 190iSup_lesup_le · cited by 159sup_lele_sup_of_le_left · cited by 26le_sup_of_le_leftle_sup_of_le_right · cited by 17le_sup_of_le_rightiSup_comp_le · cited by 4iSup_comp_leiSup_orCITED BYCITES

Cites9

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

Cited by3

Results whose statement or proof uses this declaration.