closure_closure_coe_preimage — Mathlib

English

For any subset k of G, the closure of the preimage of k under the inclusion map from closure(k) to G is the whole group, i.e., closure(((↑) : closure(k) → G)^{-1} k) = ⊤.

Русский

Для любого подмножества k группы G замыкание предобраза k по включению из closure(k) в G равно всей группе: closure((↑)^{-1}(k)) = ⊤.

LaTeX

$$$ \operatorname{closure}\big( (\iota: \mathrm{closure}(k) \to G)^{-1}(k) \big) = \top $$$

Lean4

@[to_additive (attr := simp)]
theorem closure_closure_coe_preimage {k : Set G} : closure (((↑) : closure k → G) ⁻¹' k) = ⊤ :=
  eq_top_iff.2 fun x _ ↦
    Subtype.recOn x fun _ hx' ↦
      closure_induction (fun _ h ↦ subset_closure h) (one_mem _) (fun _ _ _ _ ↦ mul_mem) (fun _ _ ↦ inv_mem) hx'

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