truncatedInf_sups — Mathlib

English

If s and t have infs, then truncatedInf (s ⊼ t) a equals truncatedInf s a ⊓ truncatedInf t a.

Русский

Если существуют inf' для s и t, то truncatedInf(s ⊼ t) a = truncatedInf s a ⊓ truncatedInf t a.

LaTeX

$$$\operatorname{truncatedInf}(s \sqcap t) \, a = \operatorname{truncatedInf} s \, a \sqcap \operatorname{truncatedInf} t \, a$$$

Lean4

theorem truncatedInf_sups (hs : a ∈ upperClosure s) (ht : a ∈ upperClosure t) :
    truncatedInf (s ⊻ t) a = truncatedInf s a ⊔ truncatedInf t a :=
  by
  simp only [truncatedInf_of_mem, hs, ht, sups_aux.2 ⟨hs, ht⟩, inf'_sup_inf', filter_sups_le]
  simp_rw [← image_sup_product]
  rw [inf'_image]
  simp [Function.uncurry_def]

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