mem_localized₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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