mono — Mathlib

English

If hs is a strong antichain with respect to r₁, and r₂ ≤ r₁, then hs is a strong antichain with respect to r₂.

Русский

Если s является сильной антицепью относительно r₁, и r₂ ≤ r₁, то s является сильной антицепью относительно r₂.

LaTeX

$$$\\text{IsStrongAntichain}(r_1, s) \\land r_2 \\le r_1 \\Rightarrow \\text{IsStrongAntichain}(r_2, s)$$$

Lean4

theorem mono (hs : IsStrongAntichain r₁ s) (h : r₂ ≤ r₁) : IsStrongAntichain r₂ s :=
  hs.mono' fun _ _ hab c => (hab c).imp (compl_le_compl h _ _) (compl_le_compl h _ _)

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