English
For s and t with a ∈ upperClosure s and a ∈ upperClosure t, truncatedInf (s ⊻ t) a = truncatedInf s a ⊔ truncatedInf t a.
Русский
Для s и t с a ∈ upperClosure s, a ∈ upperClosure t: truncatedInf (s ⊻ t) a = truncatedInf s a ⊔ truncatedInf t a.
LaTeX
$$$a \in \operatorname{upperClosure}(s) \land a \in \operatorname{upperClosure}(t) \Rightarrow \operatorname{truncatedInf}(s \odot t) \, a = \operatorname{truncatedInf} s \, a \sqcup \operatorname{truncatedInf} t \, a$$$
Lean4
theorem truncatedSup_infs (hs : a ∈ lowerClosure s) (ht : a ∈ lowerClosure t) :
truncatedSup (s ⊼ t) a = truncatedSup s a ⊓ truncatedSup t a :=
by
simp only [truncatedSup_of_mem, hs, ht, infs_aux.2 ⟨hs, ht⟩, sup'_inf_sup', filter_infs_le]
simp_rw [← image_inf_product]
rw [sup'_image]
simp [Function.uncurry_def]
