truncatedInf_union — Mathlib

English

Symmetric to Union Left: if a ∉ upperClosure s and a ∈ upperClosure t, then truncatedInf (s ∪ t) a = truncatedInf t a.

Русский

Симметрично: если a ∉ upperClosure s и a ∈ upperClosure t, тогда truncatedInf(s ∪ t) a = truncatedInf t a.

LaTeX

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

Lean4

theorem truncatedInf_union (hs : a ∈ upperClosure s) (ht : a ∈ upperClosure t) :
    truncatedInf (s ∪ t) a = truncatedInf s a ⊓ truncatedInf t a := by
  simpa only [truncatedInf_of_mem, hs, ht, upper_aux.2 (Or.inl hs), filter_union] using inf'_union _ _ _

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