monotone_or — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{Monotone}(p) \\to \\text{Monotone}(q) \\to \\text{Monotone}(x \\mapsto p(x) \\lor q(x))$$$

Lean4

theorem monotone_or {p q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) : Monotone fun x => p x ∨ q x := fun _ _ h =>
  Or.imp (m_p h) (m_q h)

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