inter_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

/-- The intersection of a chain and an antichain is subsingleton. -/
theorem inter_subsingleton_of_isChain_of_isAntichain (hs : IsChain r s) (ht : IsAntichain r t) : (s ∩ t).Subsingleton :=
  subsingleton_of_isChain_of_isAntichain (hs.mono (by simp)) (ht.subset (by simp))

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