imp_on — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem imp_on (h : s.Pairwise r) (hrp : s.Pairwise fun ⦃a b : α⦄ => r a b → p a b) : s.Pairwise p :=
  fun _a ha _b hb hab => hrp ha hb hab <| h ha hb hab

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