subsingleton — Mathlib

English

If α is directed with respect to r and s is a strong antichain, then s is a subsingleton.

Русский

Если α направлено относительно r, и s является сильной антицепью, то s — подсинглтон.

LaTeX

$$$[\\text{IsDirected}(\\alpha, r)](h) \\Rightarrow \\text{IsStrongAntichain}(r, s) \\Rightarrow s.\\text{Subsingleton}$$$

Lean4

protected theorem subsingleton [IsDirected α r] (h : IsStrongAntichain r s) : s.Subsingleton := fun a ha b hb =>
  let ⟨_, hac, hbc⟩ := directed_of r a b
  h.eq ha hb hac hbc

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