Satisfaction in an indexed family of structures

Classical satisfaction at an index of a structure family interp : W → L.Structure M — mathlib's Formula.Realize with the instance selected per index — and the transport of the Formula.realize_* simp set. [UPSTREAM] candidate for Mathlib/ModelTheory, which carries one structure at a time.

def FirstOrder.Language.Formula.RealizeAt {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (ψ : L.Formula α) (interp : W → L.Structure M) (w : W) (v : α → M) : Prop

Satisfaction at an index of a structure family: mathlib's Formula.Realize in the structure the family carries at w.

Equations

• ψ.RealizeAt interp w v = ψ.Realize v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_not {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ : L.Formula α) : ψ.not.RealizeAt interp w v ↔ ¬ψ.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_inf {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ₁ ψ₂ : L.Formula α) : (ψ₁ ⊓ ψ₂).RealizeAt interp w v ↔ ψ₁.RealizeAt interp w v ∧ ψ₂.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_sup {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) (ψ₁ ψ₂ : L.Formula α) : (ψ₁ ⊔ ψ₂).RealizeAt interp w v ↔ ψ₁.RealizeAt interp w v ∨ ψ₂.RealizeAt interp w v

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_all₁ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) [DecidableEq α] (x : α) (ψ : L.Formula α) : (all₁ x ψ).RealizeAt interp w v ↔ ∀ (d : M), ψ.RealizeAt interp w (Function.update v x d)

@[simp]

theorem FirstOrder.Language.Formula.realizeAt_ex₁ {L : Language} {W : Type u_1} {M : Type u_2} {α : Type u_3} (interp : W → L.Structure M) (w : W) (v : α → M) [DecidableEq α] (x : α) (ψ : L.Formula α) : (ex₁ x ψ).RealizeAt interp w v ↔ ∃ (d : M), ψ.RealizeAt interp w (Function.update v x d)