truncatedSup_union — Mathlib

English

If a belongs to the lower closure of s and t, then truncatedSup of s ∪ t at a equals the join of truncatedSup s a and truncatedSup t a.

Русский

Пусть a ∈ нижнего замыкания s и t. Тогда truncatedSup(s ∪ t) a = truncatedSup s a ⊔ truncatedSup t a.

LaTeX

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

Lean4

theorem truncatedSup_union (hs : a ∈ lowerClosure s) (ht : a ∈ lowerClosure t) :
    truncatedSup (s ∪ t) a = truncatedSup s a ⊔ truncatedSup t a := by
  simpa only [truncatedSup_of_mem, hs, ht, lower_aux.2 (Or.inl hs), filter_union] using sup'_union _ _ _

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