mem_left_iff_eq_zero_of_disjoint — Mathlib

English

Symmetric to the previous: for disjoint p and p', any x ∈ p' satisfies x ∈ p iff x = 0.

Русский

Симметрично к предыдущему: для несовместимых 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_left_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 hx x.2, fun h => h.symm ▸ p.zero_mem⟩

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