monotone_and — Mathlib

English

If p and q are monotone predicates on a preorder, then the conjunction x ↦ p(x) ∧ q(x) is monotone.

Русский

Если p и q — монотонные предикаты на предордере, то конъюнкция x ↦ p(x) ∧ q(x) монотонна.

LaTeX

$$$\\text{Monotone}(p) \\,\\land \\, \\text{Monotone}(q) \\Rightarrow \\text{Monotone}(x \\mapsto p(x) \\land q(x))$$$

Lean4

theorem monotone_and {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun x => p x ∧ q x :=
  fun _ _ h =>
  And.imp (m_p h)
    (m_q h)
      -- Note: by finish [monotone] doesn't work

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