disjoint_def — Mathlib

English

Two subgroups H1 and H2 are disjoint iff the only element common to both is the identity.

Русский

Две подгруппы H1 и H2 должны не иметь общих элементов, кроме единицы.

LaTeX

$$$ Disjoint(H_1,H_2) \\iff \\forall x \\in H_1, x \\in H_2 \\implies x = 1 $$$

Lean4

@[to_additive]
theorem disjoint_def {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1 :=
  disjoint_iff_inf_le.trans <| by simp only [SetLike.le_def, mem_inf, mem_bot, and_imp]

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