Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.realize_ex

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {θ : L.BoundedFormula α l.succ}
  {v : α → M} {xs : Fin l → M}, θ.ex.Realize v xs ↔ ∃ a, θ.Realize v (Fin.snoc xs a)

Defined in

Mathlib.ModelTheory.Semantics

Cited by

2 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.Structure