mono

Mathlib.Data.Set.Monotone

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

English

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

Русский

Если f строго антитонична на s и s2 ⊆ s, то f строго антитонична на s2.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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