subset — Mathlib

English

For a complete type p, the theory on T with constants α is contained in p's complete theory: (L.lhomWithConstants α).onTheory T ⊆ p.

Русский

Для полного типа p теория на T с константами α включена в полную теорию p: (L.lhomWithConstants α).onTheory T ⊆ p.

LaTeX

$$$(L.lhomWithConstants α).onTheory T \\\\subseteq (p : L[[α]].Theory)$$$

Lean4

theorem subset (p : T.CompleteType α) : (L.lhomWithConstants α).onTheory T ⊆ (p : L[[α]].Theory) :=
  p.subset'

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