subtheoryModel — Mathlib

English

A model of a theory M carries a subtheory; it remains a model for any subtheory T'.

Русский

У модели теории M сохраняется свойство быть моделью любой подтеории T'.

LaTeX

$$$\text{If } M \models T \text{ and } T' \subseteq T, \text{ then } M \models T'.$$$

Lean4

/-- A model of a theory is also a model of any subtheory. -/
@[simps]
def subtheoryModel (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T) : T'.ModelType
    where
  Carrier := M
  is_model := ⟨fun _φ hφ => realize_sentence_of_mem T (h hφ)⟩

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