strictMonoOn

Mathlib.Data.Set.Subsingleton

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.strictMonoOn

English

If s is a subsingleton, then f is strictly monotone on s: for a,b ∈ s, a < b implies f(a) < f(b).

Русский

Если s — пододиноство, то f строго монотонна на s: для a,b ∈ s, если a < b, то f(a) < f(b).

LaTeX

$$$ \forall x,y \in s, x < y \Rightarrow f(x) < f(y)$$$

Lean4

protected theorem strictMonoOn (h : s.Subsingleton) : StrictMonoOn f s := fun _ ha _ hb hlt => (hlt.ne (h ha hb)).elim

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru