truncatedSup_union_right — Mathlib

English

If a ∉ lowerClosure s and a ∈ lowerClosure t, then truncatedSup(s ∪ t) a = truncatedSup t a.

Русский

Если a ∉ нижнего замыкания s и a ∈ нижнего замыкания t, тогда truncatedSup(s ∪ t) a = truncatedSup t a.

LaTeX

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

Lean4

theorem truncatedSup_union_right (hs : a ∉ lowerClosure s) (ht : a ∈ lowerClosure t) :
    truncatedSup (s ∪ t) a = truncatedSup t a := by rw [union_comm, truncatedSup_union_left ht hs]

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