mem_mk — Mathlib

English

There exists a Subsemigroup mk(s, h) built from a set s with a closure condition h; for every x, x ∈ mk(s, h) iff x ∈ s.

Русский

Существует подподполугруппа mk(s, h), построенная из множества s с условием замыкания h; для любого x верно x ∈ mk(s, h) ⇔ x ∈ s.

LaTeX

$$$ x \\in \\operatorname{mk}(s, h_{\\mathrm{mul}}) \\iff x \\in s $$$

Lean4

@[to_additive (attr := simp)]
theorem mem_mk {s : Set M} {x : M} (h_mul) : x ∈ mk s h_mul ↔ x ∈ s :=
  Iff.rfl

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