closure_closure_coe_preimage — Mathlib

English

For any subset s of M, the closure of the preimage of s under the inclusion ι: closure s → M equals the top submonoid of closure s.

Русский

Для любого подмножества s ⊆ M замыкание предобраза s через включение ι: closure s → M дает верхний подмножод closure s.

LaTeX

$$$ \operatorname{closure}\big( \operatorname{Set.preimage}(\operatorname{Subtype.val})\, s \big) = \top$.$$

Lean4

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

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