closure_closure_coe_preimage — Mathlib

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'

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