insert — Mathlib

English

If T is universal and φ is universal, then inserting φ into T yields a universal theory.

Русский

Если T универсальна и φ универсальна, то вставка φ в T даёт универсальную теорию.

LaTeX

$$$(T.Insert(\varphi)).IsUniversal$$$

Lean4

theorem insert {T : L.Theory} [hT : T.IsUniversal] {φ : L.Sentence} (hφ : φ.IsUniversal) : (insert φ T).IsUniversal :=
  ⟨by
    simp only [Set.mem_insert_iff, forall_eq_or_imp, hφ, true_and]
    exact hT.isUniversal_of_mem⟩

Похожие утверждения