English
The L[[A]]-closure of s equals the A-constants expansion of the L-closure of A ∪ s; i.e., closure in the language with constants A of s is the same as the constants-extended closure of A ∪ s in L.
Русский
Замыкание в языке с константами A от s равно константному расширению замыкания L от A ∪ s.
LaTeX
$$$ \operatorname{closure}_{L[[A]]}(s) = \operatorname{withConstants}_L(A, \operatorname{closure}_L(A \cup s)) $$$
Lean4
theorem closure_withConstants_eq :
closure (L[[A]]) s = (closure L (A ∪ s)).withConstants ((A.subset_union_left).trans subset_closure) :=
by
refine closure_eq_of_le ((A.subset_union_right).trans subset_closure) ?_
rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct, Set.union_subset_iff,
and_true]
exact subset_closure_withConstants
