subset — Mathlib

English

If s is a strong antichain with respect to r, and t ⊆ s, then t is also a strong antichain with respect to r.

Русский

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

LaTeX

$$$\\text{IsStrongAntichain}(r, s) \\land t \\subseteq s \\Rightarrow \\text{IsStrongAntichain}(r, t)$$$

Lean4

protected theorem subset (hs : IsStrongAntichain r s) (h : t ⊆ s) : IsStrongAntichain r t :=
  hs.mono h

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