monotone_distinctConstantsTheory — Mathlib

English

The assignment s ↦ distinctConstantsTheory(s) is monotone with respect to inclusion: s ⊆ t implies distinctConstantsTheory(s) ⊆ distinctConstantsTheory(t).

Русский

Отображение, отправляющее множество констант в соответствующую теорию, монотонно по включению: если s ⊆ t, то distinctConstantsTheory(s) ⊆ distinctConstantsTheory(t).

LaTeX

$$$s \\subseteq t \\Rightarrow L.\\mathrm{distinctConstantsTheory}(s) \\subseteq L.\\mathrm{distinctConstantsTheory}(t)$$$

Lean4

theorem monotone_distinctConstantsTheory : Monotone (L.distinctConstantsTheory : Set α → L[[α]].Theory) :=
  fun _s _t st => L.distinctConstantsTheory_mono st

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