maximal_mem_lowerClosure_iff_mem — Mathlib

English

Let s be an antichain in a poset. An element x is maximal in the lower closure of s if and only if x ∈ s.

Русский

Пусть s является антицепью в частично упорядоченном множестве. Элемент x максимален в нижнем замыкании s тогда и только тогда, когда x ∈ s.

LaTeX

$$$ \\operatorname{Maximal}(x \\in \\operatorname{lowerClosure}(s)) \\ x \\iff x \\in s $$$

Lean4

theorem maximal_mem_lowerClosure_iff_mem (hs : IsAntichain (· ≤ ·) s) : Maximal (· ∈ lowerClosure s) x ↔ x ∈ s :=
  hs.to_dual.minimal_mem_upperClosure_iff_mem

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