no goals
α : Type u_2
β : Type u_1
γ : Type ?u.817681
δ : Type ?u.817684
inst✝² : MeasurableSpace α
K : Type ?u.817690
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : MeasurableSet s
x : α
⊢ ↑(restrict f s) x ≤ ↑(restrict g s) x
simp only [coe_restrict _ hs, indicator_le_indicator (H x)]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.817681
δ : Type ?u.817684
inst✝² : MeasurableSpace α
K : Type ?u.817690
inst✝¹ : Zero β
inst✝ : Preorder β
s : Set α
f g : α →ₛ β
H : f ≤ g
hs : ¬MeasurableSet s
⊢ restrict f s ≤ restrict g s
simp only [restrict_of_not_measurable hs, le_refl]