mem_invSubmonoid_iff_exists_mk' — Mathlib

English

An element x lies in invSubmonoid M S iff there exists m ∈ M with x = mk' S 1 m.

Русский

Элемент x принадлежит invSubmonoid M S тогда и только тогда, когда существует m ∈ M с x = mk' S 1 m.

LaTeX

$$$x \in invSubmonoid M S \iff \exists m:\, M,\; mk' S 1 m = x$$$

Lean4

theorem mem_invSubmonoid_iff_exists_mk' (x : S) : x ∈ invSubmonoid M S ↔ ∃ m : M, mk' S 1 m = x :=
  by
  simp_rw [← toInvSubmonoid_eq_mk']
  exact
    ⟨fun h => ⟨_, congr_arg Subtype.val (toInvSubmonoid_surjective M S ⟨x, h⟩).choose_spec⟩, fun h =>
      h.choose_spec ▸ (toInvSubmonoid M S h.choose).prop⟩

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