le_comap_primeCompl_iff — Mathlib

English

Comparison lemma: I.primeCompl ≤ J.primeCompl.comap f iff J.comap f ≤ I, for prime J and a map f.

Русский

Лемма сравнения: I.primeCompl ≤ J.primeCompl.comap f эквивалентно J.comap f ≤ I, при J простом и отображении f.

LaTeX

$$$$ I.{\rm primeCompl} \le J.{\rm primeCompl}.comap f \;\Longleftrightarrow\; J .\mathrm{comap} f \le I $$$$

Lean4

theorem le_comap_primeCompl_iff {J : Ideal P} [J.IsPrime] {f : R →+* P} :
    I.primeCompl ≤ J.primeCompl.comap f ↔ J.comap f ≤ I :=
  ⟨fun h x hx => by
    contrapose! hx
    exact h hx, fun h _ hx hfxJ => hx (h hfxJ)⟩

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