spanNorm_eq_bot_iff — Mathlib

English

For CharZero S, the set { I ∈ (Ideal S)⁰ | absNorm(I) ≤ n } is finite.

Русский

Для CharZero(S) множество { I ∈ (Ideal S)⁰ | absNorm(I) ≤ n } конечно.

LaTeX

$$$$\forall n\in \mathbb{N},\; \{ I:\ I\in (\mathrm{Ideal}(S))^{0} \mid \operatorname{absNorm}(I) \le n\} \text{finite}. $$$$

Lean4

@[simp]
theorem spanNorm_eq_bot_iff {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥ := by
  simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def, map, mem_bot]

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