mem_right_iff_eq_zero_of_disjoint

English

For disjoint p and p', any x ∈ p has x ∈ p' if and only if x = 0 in M.

Русский

Для несовместимых p и p' любое x ∈ p удовлетворяет x ∈ p' тогда и только тогда, когда x = 0.

LaTeX

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

Lean4

theorem mem_right_iff_eq_zero_of_disjoint {p p' : Submodule R M} (h : Disjoint p p') {x : p} : (x : M) ∈ p' ↔ x = 0 :=
  ⟨fun hx => coe_eq_zero.1 <| disjoint_def.1 h x x.2 hx, fun h => h.symm ▸ p'.zero_mem⟩

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