truncatedSup_union_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem truncatedSup_union_left (hs : a ∈ lowerClosure s) (ht : a ∉ lowerClosure t) :
    truncatedSup (s ∪ t) a = truncatedSup s a :=
  by
  simp only [mem_lowerClosure, mem_coe, not_exists, not_and] at ht
  simp only [truncatedSup_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty, lower_aux.2 (Or.inl hs)]

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