finite_of_partiallyWellOrderedOn — Mathlib

English

If ha is an antichain with respect to r within s and hp is s PWOn by r, then s is finite.

Русский

Если ha является антицепью относительно r внутри s и hp: s PWOn по r, тогда s является конечным множеством.

LaTeX

$$$ha IsAntichain r s \\land hp: s.PartiallyWellOrderedOn r \\Rightarrow s.Finite$$$

Lean4

theorem _root_.IsAntichain.finite_of_partiallyWellOrderedOn (ha : IsAntichain r s) (hp : s.PartiallyWellOrderedOn r) :
    s.Finite := by
  refine not_infinite.1 fun hi => ?_
  obtain ⟨m, n, hmn, h⟩ := hp (hi.natEmbedding _)
  exact
    hmn.ne
      ((hi.natEmbedding _).injective <|
        Subtype.val_injective <| ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

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