Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_def

∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ) (x_1 : L.BoundedFormula α x)
  (x_2 : ↥x_1.freeVarFinset → β),
  x_1.restrictFreeVar x_2 =
    match x, x_1, x_2 with
    | _n, FirstOrder.Language.BoundedFormula.falsum, _f => FirstOrder.Language.BoundedFormula.falsum
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂, f =>
      FirstOrder.Language.BoundedFormula.equal (t₁.restrictVarLeft (f ∘ Set.inclusion ⋯))
        (t₂.restrictVarLeft (f ∘ Set.inclusion ⋯))
    | _n, FirstOrder.Language.BoundedFormula.rel R ts, f =>
      FirstOrder.Language.BoundedFormula.rel R fun i => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
    | _n, φ₁.imp φ₂, f => (φ₁.restrictFreeVar (f ∘ Set.inclusion ⋯)).imp (φ₂.restrictFreeVar (f ∘ Set.inclusion ⋯))
    | _n, φ.all, f => (φ.restrictFreeVar f).all

Defined in

Mathlib.ModelTheory.Semantics

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq