setOf_maximal_antichain — Mathlib

English

For any predicate P, the set {x | Maximal P x} is an antichain with respect to ≤.

Русский

Для произвольного предиката P множество {x | Maximal P x} является антицепью относительно ≤.

LaTeX

$$$\\operatorname{IsAntichain}(\\le, \\{x \\mid \\operatorname{Maximal} P x\\})$$$

Lean4

theorem setOf_maximal_antichain (P : α → Prop) : IsAntichain (· ≤ ·) {x | Maximal P x} := fun _ hx _ ⟨hy, _⟩ hne hle ↦
  hne (hle.antisymm <| hx.2 hy hle)

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