theorem
monotonicity.pi
{α : Sort u}
{p q : α → Prop}
(h : ∀ (a : α), implies (p a) (q a)) :
implies (∀ (a : α), p a) (∀ (a : α), q a)
theorem
monotonicity.imp
{p p' q q' : Prop}
(h₁ : implies p' q')
(h₂ : implies q p) :
implies (p → p') (q → q')
theorem
monotonicity.exists
{α : Sort u}
{p q : α → Prop}
(h : ∀ (a : α), implies (p a) (q a)) :
implies (∃ (a : α), p a) (∃ (a : α), q a)