Theorems · Theorem · logic and foundations

FirstOrder.Language.Substructure.realize_boundedFormula_top

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u_3} {n : ℕ} {φ : L.BoundedFormula α n}
  {v : α → ↥⊤} {xs : Fin n → ↥⊤}, φ.Realize v xs ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)

Defined in

Mathlib.ModelTheory.Substructures

Cited by

0 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.Structure