mem_quotient_iff_mem_sup — Mathlib

English

A membership in the image of J under the quotient map equals membership in the supremum J ⊔ I exactly when the image is taken from I to J.

Русский

Членство в образе J под факторизацией равно членству в нижнем пределе J ⊔ I тогда, когда образ зафиксирован через I и J.

LaTeX

$$$\quotient.mk I x \in J.map(\quotient.mk I) \;∼∼ x \in J \uplus I$$$

Lean4

/-- See also `Ideal.mem_quotient_iff_mem` in case `I ≤ J`. -/
@[simp]
theorem mem_quotient_iff_mem_sup {I J : Ideal R} [I.IsTwoSided] {x : R} :
    Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J ⊔ I := by
  rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ← ker_eq_comap_bot, mk_ker]

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