truncatedInf_union_left — Mathlib

English

If a ∉ upperClosure s and a ∉ upperClosure t, then truncatedInf (s ∪ t) a = ⊥.

Русский

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

LaTeX

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

Lean4

theorem truncatedInf_union_left (hs : a ∈ upperClosure s) (ht : a ∉ upperClosure t) :
    truncatedInf (s ∪ t) a = truncatedInf s a :=
  by
  simp only [mem_upperClosure, mem_coe, not_exists, not_and] at ht
  simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty, upper_aux.2 (Or.inl hs)]

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