inter_subsingleton_of_isAntichain_of_isChain

English

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

Русский

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

LaTeX

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

Lean4

/-- The intersection of an antichain and a chain is subsingleton. -/
theorem inter_subsingleton_of_isAntichain_of_isChain (hs : IsAntichain r s) (ht : IsChain r t) : (s ∩ t).Subsingleton :=
  inter_comm _ _ ▸ inter_subsingleton_of_isChain_of_isAntichain ht hs

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