truncatedSup_union_of_notMem — Mathlib

English

If a is not in the upper closure of s nor in that of t, then truncatedSup(s ∪ t) a = ⊤.

Русский

Если a не принадлежит верхнему замыканию ни s, ни t, то truncatedSup(s ∪ t) a = ⊤.

LaTeX

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

Lean4

theorem truncatedSup_union_of_notMem (hs : a ∉ lowerClosure s) (ht : a ∉ lowerClosure t) : truncatedSup (s ∪ t) a = ⊤ :=
  truncatedSup_of_notMem fun h ↦ (lower_aux.1 h).elim hs ht

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