English
For a formula of the form φ.iAlls β with a finite index β, (φ.iAlls β).Realize v is equivalent to ∀ i : β → M, φ.Realize (fun a => Sum.elim v i a).
Русский
Для формулы вида φ.iAlls β с конечным β, (φ.iAlls β).Realize v эквивалентно ∀ i : β → M, φ.Realize (fun a => Sum.elim v i a).
LaTeX
$$$(\varphi.iAlls \beta).Realize v \iff \forall i : \beta \to M, \varphi.Realize (fun a => Sum.elim v i a)$$$
Lean4
@[simp]
theorem _root_.FirstOrder.Language.Formula.realize_iAlls [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} :
(φ.iAlls β).Realize v ↔ ∀ (i : β → M), φ.Realize (fun a => Sum.elim v i a) :=
by
let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin β))
rw [Formula.iAlls]
simp only [Nat.add_zero, realize_alls, realize_relabel, Function.comp_def, castAdd_zero, Sum.elim_map, id_eq]
refine Equiv.forall_congr ?_ ?_
·
exact
⟨fun v => v ∘ e, fun v => v ∘ e.symm, fun _ => by simp [Function.comp_def], fun _ => by simp [Function.comp_def]⟩
· intro x
rw [Formula.Realize, iff_iff_eq]
congr
funext i
exact i.elim0
