maximal_mem_iff — Mathlib

English

Let (A, ≤) be a preorder and S ⊆ A an antichain with respect to ≤. Then for every a in A, a is a maximal element of S with respect to ≤ if and only if a ∈ S.

Русский

Пусть (A, ≤) — предупорядоченное множество и S ⊆ A антицепь относительно ≤. Тогда для каждого элемента a ∈ A выполняется: a — максимальный элемент S по отношению к ≤ тогда и только тогда, когда a ∈ S.

LaTeX

$$$\\operatorname{IsAntichain}(\\le, s) \\Rightarrow \\forall a, \\operatorname{Max}_{\\le}(a; s) \\iff a \\in s$$$

Lean4

theorem maximal_mem_iff (hs : IsAntichain (· ≤ ·) s) : Maximal (· ∈ s) a ↔ a ∈ s :=
  hs.to_dual.minimal_mem_iff

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