mono

Mathlib.Data.Set.Monotone

URI: https://scilib.ai/kg/mathlib#MonotoneOn.mono

English

If a function f is monotone on a set s and s2 is a subset of s, then f is monotone on s2.

Русский

Если функция f монотонна на множестве s и s2 ⊆ s, то f монотонна на s2.

LaTeX

$$$\operatorname{MonotoneOn}(f,s) \to (s_2 \subseteq s) \to \operatorname{MonotoneOn}(f,s_2)$$$

Lean4

theorem _root_.MonotoneOn.mono (h : MonotoneOn f s) (h' : s₂ ⊆ s) : MonotoneOn f s₂ := fun _ hx _ hy =>
  h (h' hx) (h' hy)

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

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

Разделы

Аффилиация

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