mono'

Mathlib.Data.Set.Pairwise.Basic

URI: https://scilib.ai/kg/mathlib#Set.Pairwise.mono'

English

If r is bounded above by p (r ≤ p) and s is pairwise with respect to r, then s is pairwise with respect to p.

Русский

Если r ≤ p и s попарно по r, то попарно по p.

LaTeX

$$$\forall {\alpha} {r p : \alpha \to \alpha \to \mathrm{Prop}} {s : Set \alpha}, (\forall a b, r a b \to p a b) \to s.Pairwise r \to s.Pairwise p$$$

Lean4

theorem mono' (H : r ≤ p) (hr : s.Pairwise r) : s.Pairwise p :=
  hr.imp H

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

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

Разделы

Аффилиация

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