noncomputable def juxt {S : Type u_1} {E : Type u_2} (Λ : Set S) (η : S → E) (ζ : ↑Λ → E) (x : S) : E

Equations

• juxt Λ η ζ x = if h : x ∈ Λ then ζ ⟨x, h⟩ else η x

theorem juxt_apply_of_mem {S : Type u_1} {E : Type u_2} {Λ : Set S} {η : S → E} {x : S} (hx : x ∈ Λ) (ζ : ↑Λ → E) : juxt Λ η ζ x = ζ ⟨x, hx⟩

theorem juxt_apply_of_not_mem {S : Type u_1} {E : Type u_2} {Λ : Set S} {η : S → E} {x : S} (h : x ∉ Λ) (ζ : ↑Λ → E) : juxt Λ η ζ x = η x

theorem measurable_coordinate_projection_2 {S : Type u_1} {E : Type u_2} {𝓔 : MeasurableSpace E} {Δ : Set S} {x : S} (h : x ∈ Δ) : Measurable fun (σ : S → E) => σ x

theorem Measurable.juxt {S : Type u_1} {E : Type u_2} {𝓔 : MeasurableSpace E} {Λ : Set S} {η : S → E} : Measurable (juxt Λ η)