isChain_and_isAntichain_iff_subsingleton

English

A set is simultaneously a chain and an antichain if and only if it is subsingleton.

Русский

Множество является одновременно цепью и антицепочкой тогда и только тогда, когда оно subsingleton.

LaTeX

$$$IsChain r s \land IsAntichain r s \iff s.Subsingleton$$$

Lean4

theorem isChain_and_isAntichain_iff_subsingleton : IsChain r s ∧ IsAntichain r s ↔ s.Subsingleton :=
  ⟨fun h ↦ subsingleton_of_isChain_of_isAntichain h.1 h.2, fun h ↦ ⟨h.isChain, h.isAntichain _⟩⟩

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