setOf_minimal_antichain — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem setOf_minimal_antichain (P : α → Prop) : IsAntichain (· ≤ ·) {x | Minimal P x} :=
  (setOf_maximal_antichain (α := αᵒᵈ) P).swap

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