mono

Mathlib.Data.Set.Monotone

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

English

If f is antitone on s and s2 ⊆ s, then f is antitone on s2.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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