truncatedSup_of_isAntichain — Mathlib

English

If s is an antichain with respect to ≤, and a ∈ s, then the truncatedSup of s at a equals a.

Русский

Если множество s является антиподом относительно ≤ и a ∈ s, то truncatedSup s a = a.

LaTeX

$$$\text{If } s\text{ is an antichain and } a\in s,\; \operatorname{truncatedSup} s \, a = a$$$

Lean4

theorem truncatedSup_of_isAntichain (hs : IsAntichain (· ≤ ·) (s : Set α)) (ha : a ∈ s) : truncatedSup s a = a :=
  by
  refine le_antisymm ?_ le_truncatedSup
  simp_rw [truncatedSup_of_mem (subset_lowerClosure ha), sup'_le_iff, mem_filter]
  rintro b ⟨hb, hab⟩
  exact (hs.eq ha hb hab).ge

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