mono — Mathlib

English

If s is an antichain with respect to r1 and r2 ≤ r1, then s is an antichain with respect to r2.

Русский

Если s является антицепью относительно r1 и r2 ≤ r1, то s является антицепью относительно r2.

LaTeX

$$$IsAntichain(r2,s) \\text{ whenever } IsAntichain(r1,s) \\text{ and } r2 \le r1$$$

Lean4

theorem mono (hs : IsAntichain r₁ s) (h : r₂ ≤ r₁) : IsAntichain r₂ s :=
  hs.mono' <| compl_le_compl h

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