R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ jacobson I
⊢ x ∈ jacobson J
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
⊢ I ≤ J → jacobson I ≤ jacobson J
intro h x hx
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
h : I ≤ J
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ IsMaximal J_1} → x ∈ I
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ jacobson I
⊢ x ∈ jacobson J
erw [mem_sInf] at hx⊢
no goals
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I✝ I J : Ideal R
h : I ≤ J
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ IsMaximal J} → x ∈ I_1
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ IsMaximal J_1} → x ∈ I
exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩