iInf_pow_smul — Mathlib

English

The infimum over all natural powers of I acting on the top submodule is the bottom submodule: ∨_n I^n • ⊤ = ⊥.

Русский

Нижний предел последовательности I^n действует на верхний подмодуль и совпадает с нулем: ∨_n I^n • ⊤ = ⊥.

LaTeX

$$$\bigwedge_{n \in \mathbb{N}} (I^n \cdot \top) = \bot$$$

Lean4

theorem iInf_pow_smul (h : IsHausdorff I M) : (⨅ n : ℕ, I ^ n • ⊤ : Submodule R M) = ⊥ :=
  eq_bot_iff.2 fun x hx => (mem_bot _).2 <| h.haus x fun n => SModEq.zero.2 <| (mem_iInf fun n : ℕ => I ^ n • ⊤).1 hx n

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