realize_iInf — Mathlib

English

If f is a finite family of bounded formulas indexed by β, then (iInf f).Realize v v' holds iff ∀ b, (f b).Realize v v'.

Русский

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

LaTeX

$$$(\mathrm{iInf} f).Realize v v' \iff \forall b, (f b).Realize v v'$$$

Lean4

@[simp]
theorem realize_iInf [Finite β] {f : β → L.BoundedFormula α n} {v : α → M} {v' : Fin n → M} :
    (iInf f).Realize v v' ↔ ∀ b, (f b).Realize v v' := by
  simp only [iInf, realize_foldr_inf, List.mem_map, Finset.mem_toList, Finset.mem_univ, true_and, forall_exists_index,
    forall_apply_eq_imp_iff]

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