range_id

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Hom.range_id

English

As above: the L[[A]]-closure of s equals the A-constants extension of the L-closure of A ∪ s.

Русский

Как выше: замыкание L[[A]] от s равно расширению константами A замыкания L от A ∪ s.

LaTeX

$$$ \operatorname{closure}_{L[[A]]}(s) = \operatorname{withConstants}_L(A, \operatorname{closure}_L(A \cup s)) $$$

Lean4

@[simp]
theorem range_id : range (id L M) = ⊤ :=
  SetLike.coe_injective Set.range_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru