subsingleton — Mathlib

English

If r is trichotomous and s is an antichain, then s is subsingleton.

Русский

Если r тризонный и s — антицепь, то S — subsingleton.

LaTeX

$$$[IsTrichotomous(\alpha, r)] \Rightarrow IsAntichain(r,s) \Rightarrow s.Subsingleton$$$

Lean4

protected theorem subsingleton [IsTrichotomous α r] (h : IsAntichain r s) : s.Subsingleton :=
  by
  rintro a ha b hb
  obtain hab | hab | hab := trichotomous_of r a b
  · exact h.eq ha hb hab
  · exact hab
  · exact h.eq' ha hb hab

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