mono — Mathlib

English

If r is pairwise and h preserves r to p, then p is pairwise.

Русский

Если отношение r держится попарно и при каждом случае r подразумевает p, то p держится попарно.

LaTeX

$$$\\operatorname{Pairwise}(r) \\rightarrow \\bigl(\\forall i j,\, r(i,j) \\rightarrow p(i,j)\\bigr) \\rightarrow \\operatorname{Pairwise}(p)$$$

Lean4

theorem mono (hr : Pairwise r) (h : ∀ ⦃i j⦄, r i j → p i j) : Pairwise p := fun _i _j hij => h <| hr hij

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