realize_foldr_sup — Mathlib

English

For a finite list of bounded formulas l, the realization of the fold of sup over the list is equivalent to the existence of a member of the list which is realized.

Русский

Для конечного списка ограниченных формул свёртка через операцию sup реализуется тогда, когда существует элемент списка, для которого выполняется соответствующая реализация.

LaTeX

$$$ (l.\!foldr (\,\sqcup\,) \bot)^{\mathcal{M}}(v, xs) \iff \exists \phi \in l, \phi^{\mathcal{M}}(v, xs) $$$

Lean4

@[simp]
theorem realize_foldr_sup (l : List (L.BoundedFormula α n)) (v : α → M) (xs : Fin n → M) :
    (l.foldr (· ⊔ ·) ⊥).Realize v xs ↔ ∃ φ ∈ l, BoundedFormula.Realize φ v xs := by
  induction l with
  | nil => simp
  | cons φ l ih => simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or, exists_eq_left]

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