imp — Mathlib

English

If s is pairwise with respect to r and r ⇒ p, then s is pairwise with respect to p.

Русский

Если s попарно относительно r и r ⇒ p, тогда s попарно относительно p.

LaTeX

$$$\\operatorname{Set.Pairwise}(s,r) \\land \\forall a,b, r(a,b) \\Rightarrow p(a,b) \\Rightarrow \\operatorname{Set.Pairwise}(s,p)$$$

Lean4

theorem imp (h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) : s.Pairwise p :=
  h.imp_on <| pairwise_of_forall s _ hpq

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