disjoint_def — Mathlib

English

Two submodules p and p' are disjoint if their intersection is {0}, equivalently if the only common vector is the zero vector.

Русский

Два подмодуля p и p' несовместны тогда и только тогда их пересечение равно {0}.

LaTeX

$$$\\text{Disjoint}(p,p') \\iff \\forall x \\in p, \\; x \\in p' \\Rightarrow x = 0$$$

Lean4

theorem disjoint_def {p p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0 : M) :=
  disjoint_iff_inf_le.trans <| show (∀ x, x ∈ p ∧ x ∈ p' → x ∈ ({0} : Set M)) ↔ _ by simp

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