English
For [Finite γ], φ.iExs γ Realize v is equivalent to ∃ i : γ → M, φ.Realize (Sum.elim v i).
Русский
Для [ конечного γ ], φ.iExs γ Realize v эквивалентно ∃ i : γ → M, φ.Realize (Sum.elim v i).
LaTeX
$$$(\varphi.iExs \gamma).Realize v \iff \exists i : \gamma \to M, \varphi.Realize (Sum.elim v i)$$$
Lean4
@[simp]
theorem _root_.FirstOrder.Language.Formula.realize_iExs [Finite γ] {φ : L.Formula (α ⊕ γ)} {v : α → M} :
(φ.iExs γ).Realize v ↔ ∃ (i : γ → M), φ.Realize (Sum.elim v i) :=
by
let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin γ))
rw [Formula.iExs]
simp only [Nat.add_zero, realize_exs, realize_relabel, Function.comp_def, castAdd_zero, Sum.elim_map, id_eq]
refine Equiv.exists_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
