subset_closure_withConstants — Mathlib

English

Let A ⊆ S. Then every a ∈ A lies in the closure of s in the language L with constants A; i.e., A ⊆ closure_L[[A]](s).

Русский

Пусть A ⊆ S. Тогда каждый a ∈ A принадлежит замыканию s в языке L с константами A; то есть A ⊆ closure_L[[A]](s).

LaTeX

$$$ A \subseteq \operatorname{closure}_{L[[A]]}(s) $$$

Lean4

theorem subset_closure_withConstants : A ⊆ closure (L[[A]]) s :=
  by
  intro a ha
  simp only [SetLike.mem_coe]
  let a' : L[[A]].Constants := Sum.inr ⟨a, ha⟩
  exact constants_mem a'

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