disjoint_def — Mathlib

English

Two submonoids p1 and p2 are disjoint if and only if the only common element is the identity: Disjoint(p1,p2) iff ∀ x, x ∈ p1 → x ∈ p2 → x = 1.

Русский

Два подмонома p1 и p2 не пересекаются тогда и только тогда, когда единственный общий элемент — единица: Disjoint(p1,p2) ↔ ∀ x, x ∈ p1 → x ∈ p2 → x = 1.

LaTeX

$$$$\\operatorname{Disjoint}(p_1,p_2) \\iff \\forall x,\\; x \\in p_1 \\rightarrow x \\in p_2 \\rightarrow x = 1.$$$$

Lean4

@[to_additive]
theorem disjoint_def {p₁ p₂ : Submonoid M} : Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1 := by
  simp_rw [disjoint_iff_inf_le, SetLike.le_def, mem_inf, and_imp, mem_bot]

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