truncatedInf_of_isAntichain — Mathlib

English

If a ∈ upperClosure s and a ∉ upperClosure t, then truncatedInf (s ∪ t) a = truncatedInf s a.

Русский

Если a ∈ upperClosure s и a ∉ upperClosure t, тогда truncInf(s ∪ t) a = truncInf s a.

LaTeX

$$$a \in \operatorname{upperClosure}(s) \land a \notin \operatorname{upperClosure}(t) \Rightarrow \operatorname{truncatedInf}(s \cup t) \, a = \operatorname{truncatedInf} s \, a$$$

Lean4

theorem truncatedInf_of_isAntichain (hs : IsAntichain (· ≤ ·) (s : Set α)) (ha : a ∈ s) : truncatedInf s a = a :=
  by
  refine le_antisymm truncatedInf_le ?_
  simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter]
  rintro b ⟨hb, hba⟩
  exact (hs.eq hb ha hba).ge

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