truncatedInf_union_right — Mathlib

English

Symmetric variant: 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_right (hs : a ∉ upperClosure s) (ht : a ∈ upperClosure t) :
    truncatedInf (s ∪ t) a = truncatedInf t a := by rw [union_comm, truncatedInf_union_left ht hs]

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