mem_localized' — Mathlib

English

For x ∈ N, x ∈ localized'(S,p,f) iff ∃ m ∈ M′, ∃ s ∈ p with IsLocalizedModule.mk' f m s = x.

Русский

Для x ∈ N верно: x ∈ localized'(S,p,f) тогда и только тогда, когда существует m ∈ M′ и s ∈ p, такие что IsLocalizedModule.mk' f m s = x.

LaTeX

$$$x\\in\\operatorname{localized}'(S,p,f) \\iff \\exists m\\in M',\\exists s\\in p:\\ \\mathrm{IsLocalizedModule.mk'} f m s = x.$$$

Lean4

theorem mem_localized' (x : N) : x ∈ localized' S p f M' ↔ ∃ m ∈ M', ∃ s : p, IsLocalizedModule.mk' f m s = x :=
  Iff.rfl

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