haus — Mathlib

English

IsHausdorff I M implies that if x is congruent to 0 modulo I^n • ⊤ for every n, then x is 0.

Русский

IsHausdorff I M означает: если x эквивалентен 0 modulo I^n • ⊤ для всех n, то x = 0.

LaTeX

$$$\forall x \in M, \; (\forall n \in \mathbb{N}, \; x \equiv 0 \pmod{I^n \cdot \top}) \Rightarrow x = 0$$$

Lean4

theorem haus (_ : IsHausdorff I M) : ∀ x : M, (∀ n : ℕ, x ≡ 0 [SMOD (I ^ n • ⊤ : Submodule R M)]) → x = 0 :=
  IsHausdorff.haus'

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