Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.realize_iff

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
  {v : α → M} {xs : Fin l → M}, (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

Defined in

Mathlib.ModelTheory.Semantics

Cited by

7 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.Structure