mem_quotient_iff_mem — Mathlib

English

If I ≤ J, then Quotient.mk I x ∈ J.map (Quotient.mk I) is equivalent to x ∈ J.

Русский

Если I ⊆ J, то Quotient.mk I x ∈ J.map (Quotient.mk I) эквивалентно x ∈ J.

LaTeX

$$$\ Quotient.mk I x ∈ J.map(\Quotient.mk I) \iff x \in J \quad\text{when } I \le J $$$

Lean4

/-- See also `Ideal.mem_quotient_iff_mem_sup` if the assumption `I ≤ J` is not available. -/
theorem mem_quotient_iff_mem {I J : Ideal R} [I.IsTwoSided] (hIJ : I ≤ J) {x : R} :
    Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J := by rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]

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