disjoint_def' — Mathlib

English

A strengthened form: Disjoint p p' is equivalent to the condition that whenever x ∈ p and y ∈ p', and x = y, then x = 0.

Русский

Усиленная форма: Disjoint p p' эквивалентно условию, что если x ∈ p и y ∈ p', и x = y, то x = 0.

LaTeX

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

Lean4

theorem disjoint_def' {p p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = (0 : M) :=
  disjoint_def.trans ⟨fun h x hx _ hy hxy ↦ h x hx <| hxy.symm ▸ hy, fun h x hx hx' ↦ h _ hx x hx' rfl⟩

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