mem_closure_iff — Mathlib

English

Membership in closure(s) is equivalent to membership in AddSubmonoid.closure of Submonoid.closure s.

Русский

Членство в closure(s) эквивалентно членству в AddSubmonoid.closure(Submonoid.closure s).

LaTeX

$$$x \\in \\operatorname{closure}(s) \\iff x \\in AddSubmonoid.closure (Submonoid.closure s : Set R)$$$

Lean4

theorem mem_closure_iff {s : Set R} {x} : x ∈ closure s ↔ x ∈ AddSubmonoid.closure (Submonoid.closure s : Set R) :=
  Set.ext_iff.mp (coe_closure_eq s) x

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