le_spanNorm_spanNorm — Mathlib

English

For suitable tower of rings, the spanNorm at the top is controlled by a chain of spanNorms, i.e., spanNorm I ≤ spanNorm (spanNorm T I).

Русский

Для подходящей цепи колец, spanNorm верхнего уровня управляет spanNormI через цепочку: spanNorm(I) ≤ spanNorm(spanNorm(T,I)).

LaTeX

$$$$\operatorname{spanNorm}(R,I) \le \operatorname{spanNorm}(R, \operatorname{spanNorm}(T, I)).$$$$

Lean4

theorem le_spanNorm_spanNorm (I : Ideal S) : spanNorm R I ≤ spanNorm R (spanNorm T I) :=
  by
  simp_rw [spanNorm, map]
  refine span_mono ?_
  rintro _ ⟨x, hx, rfl⟩
  exact ⟨intNorm T S x, subset_span <| Set.mem_image_of_mem _ hx, by rw [intNorm_intNorm]⟩

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