Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.exs.eq_def

∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.exs =
    match x, x_1 with
    | 0, φ => φ
    | _n.succ, φ => φ.ex.exs

Defined in

Mathlib.ModelTheory.Semantics

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms