subsingleton_of_isChain_of_isAntichain

English

If s is a chain and t is an antichain with respect to r, then s ∩ t is a subsingleton.

Русский

Если s — цепь, а t — антицепочкой по отношению r, то s ∩ t является subsingleton.

LaTeX

$$$(s\cap t).Subsingleton$$$

Lean4

/-- A set which is simultaneously a chain and antichain is subsingleton. -/
theorem subsingleton_of_isChain_of_isAntichain (hs : IsChain r s) (ht : IsAntichain r s) : s.Subsingleton :=
  by
  intro x hx y hy
  by_contra! hne
  cases hs hx hy hne with
  | inl h => exact ht hx hy hne h
  | inr h => exact ht hy hx hne.symm h

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