English
There is a Galois connection between taking adjoin and forgetting the set, i.e., adjoin R s ≤ S iff s ⊆ S (as sets).
Русский
Существует связь Гало между операциями адъюнтации и забывания множества: adjoin_R(s) ≤ S тогда и только тогда, когда s ⊆ S (как множества).
LaTeX
$$$$ \\,\\\\operatorname{adjoin}_R(s) \\\\le S \\\\ \u21d4 \\\\ s \u2286 (S: Set A) $$$$
Lean4
protected theorem gc : GaloisConnection (adjoin R : Set A → NonUnitalStarSubalgebra R A) (↑) :=
by
intro s S
rw [← toNonUnitalSubalgebra_le_iff, adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_le_iff,
coe_toNonUnitalSubalgebra]
exact
⟨fun h => Set.subset_union_left.trans h, fun h =>
Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩
