English
For any subset s of M, the closure of the preimage of s under the inclusion of closure s equals the top subsemigroup of closure s.
Русский
Для любого множества s ⊆ M замыкание множества, являющегося предобразом s под инклюзией closure s, равно верхней подполугруппе closure s.
LaTeX
$$$\\operatorname{closure}((\\operatorname{Subtype.val}: \\overline{s} \\to M)^{-1}(s)) = \\top$$$
Lean4
@[to_additive (attr := simp)]
theorem closure_closure_coe_preimage {s : Set M} : closure ((Subtype.val : closure s → M) ⁻¹' s) = ⊤ :=
eq_top_iff.2 fun x _ ↦
Subtype.recOn x fun _ hx' ↦ closure_induction (fun _ h ↦ subset_closure h) (fun _ _ _ _ ↦ mul_mem) hx'