reduct_withConstants — Mathlib

English

Let S be an L-substructure of M and A ⊆ M with A ⊆ S. The L-reduct of S with constants A is exactly S; i.e., restricting the expanded structure back to the original language yields S.

Русский

Пусть S — подструктура L в M и A ⊆ M с A ⊆ S. Тогда редукция структуры, расширенной константами A, к языку L, даёт ровно S; то есть полученная структура эквивалентна S.

LaTeX

$$$ (L\ lhomWithConstants A).substructureReduct (S.withConstants h) = S $$$

Lean4

@[simp]
theorem reduct_withConstants : (L.lhomWithConstants A).substructureReduct (S.withConstants h) = S :=
  by
  ext
  simp

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