realize_iSup — Mathlib

English

If f is a finite family of bounded formulas indexed by β, then (iSup f).Realize v v' holds iff there exists b with (f b).Realize v v'.

Русский

Если f — конечное семейство ограниченных формул, индексируемых β, то realizе(iSup f) верно тогда и только тогда, когда существует индекс b такой, что (f b).Realize v v'.

LaTeX

$$$(\,\mathrm{iSup} f).Realize v v' \iff \exists b, (f b).Realize v v'$$$

Lean4

@[simp]
theorem realize_iSup [Finite β] {f : β → L.BoundedFormula α n} {v : α → M} {v' : Fin n → M} :
    (iSup f).Realize v v' ↔ ∃ b, (f b).Realize v v' := by
  simp only [iSup, realize_foldr_sup, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and, exists_exists_eq_and]

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