Mathlib Map

Theorems · Theorem · order theory

sSup_apply

∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α},
  sSup s a = ⨆ f, ↑f a
Defined in
Mathlib.Order.CompleteLattice.Basic
Cited by
2 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
SupSet
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

iSup_apply · cited by 35iSup_applyConvexOn.sSup_affine_eq · cited by 3ConvexOn.sSup_affine_eqSet · cited by 53352SetSet.Elem · cited by 7166Set.ElemiSup · cited by 2415iSupSupSet.sSup · cited by 954SupSet.sSupSupSet · cited by 154SupSetsSup_applyCITED BYCITES

Cites5

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

  • Setstatement and proof · cited by 53,352
  • Set.Elemstatement · cited by 7,166
  • iSupstatement · cited by 2,415
  • SupSet.sSupstatement · cited by 954
  • SupSetstatement and proof · cited by 154

Cited by2

Results whose statement or proof uses this declaration.