English
If c is nonempty and directed, then sSupFun hc is strictly monotone as a function of the difference (y−x).
Русский
Если c непусто и направлено, то sSupFun hc является строго монотонной функцией относительно разности (y−x).
LaTeX
$$$\\text{StrictMono}(\\,\\mathrm{sSupFun}\\; hc\\,)$$$
Lean4
theorem sSupFun_strictMono [IsOrderedAddMonoid R] {c : Set (Partial seed)} (hnonempty : c.Nonempty)
(hc : DirectedOn (· ≤ ·) c) : StrictMono (sSupFun hc) :=
by
intro x y h
apply lt_of_sub_pos
rw [← LinearPMap.map_sub]
obtain hyx := (y - x).prop
simp_rw [sSupFun, LinearPMap.domain_sSup] at hyx
obtain ⟨f, hmem, hf⟩ := (LinearPMap.mem_domain_sSup_iff (hnonempty.image _) (hc.mono_comp (by simp))).mp hyx
have : (sSupFun hc) (y - x) = f ⟨(y - x).val, hf⟩ := LinearPMap.sSup_apply _ hmem ⟨(y - x).val, hf⟩
rw [this]
obtain ⟨f', _, hf'⟩ := (Set.mem_image _ _ _).mp hmem
have hmono : StrictMono f := hf'.symm ▸ f'.prop.strictMono
rw [show 0 = f 0 by simp]
apply hmono
rw [← Subtype.coe_lt_coe]
simp [h]
