coe_withConstants — Mathlib

English

Let S be an L-substructure of M and A ⊆ M with A ⊆ S. Then the carrier of S extended by constants from A is the same as the carrier of S; i.e. the underlying set does not change when adding constants from A.

Русский

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

LaTeX

$$$ (S\text{ with constants } A) = S $$$

Lean4

@[simp]
theorem coe_withConstants : (S.withConstants h : Set M) = ↑S :=
  rfl

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