minimal_mem_upperClosure_iff_mem — Mathlib

English

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

Русский

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

LaTeX

$$$ \\operatorname{Minimal}(x \\in \\operatorname{upperClosure}(s)) \\ x \\iff x \\in s $$$

Lean4

theorem minimal_mem_upperClosure_iff_mem (hs : IsAntichain (· ≤ ·) s) : Minimal (· ∈ upperClosure s) x ↔ x ∈ s :=
  by
  simp only [upperClosure, UpperSet.mem_mk, mem_setOf_eq]
  refine ⟨fun h ↦ ?_, fun h ↦ ⟨⟨x, h, rfl.le⟩, fun b ⟨a, has, hab⟩ hbx ↦ ?_⟩⟩
  · obtain ⟨a, has, hax⟩ := h.prop
    rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]
  rwa [← hs.eq has h (hab.trans hbx)]

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