def
pointwiseSupremumOn
{ι : Type u}
{X : Type v}
{α : Type w}
[ConditionallyCompleteLattice α]
(Δ : Set ι)
(φ : X → ι → α)
:
X → α
The pointwise supremum over a parameter subset Δ of an indexed family of functions on X.
Instances For
@[simp]
theorem
pointwiseSupremumOn_apply
{ι : Type u}
{X : Type v}
{α : Type w}
[ConditionallyCompleteLattice α]
{Δ : Set ι}
{φ : X → ι → α}
{x : X}
:
pointwiseSupremumOn Δ φ x = sSup ((fun (y : ι) => φ x y) '' Δ)
Evaluating pointwiseSupremumOn Δ φ at x gives the defining supremum of the slice
y ↦ φ x y over Δ.