disjoint_def' — Mathlib

English

Disjoint H1 H2 is equivalent to the condition that whenever x ∈ H1, y ∈ H2 and x = y, then x = 1.

Русский

Не пересечение подгрупп эквивалентно: если x ∈ H1, y ∈ H2 и x = y, то x = 1.

LaTeX

$$$ Disjoint(H_1,H_2) \\iff \\forall \\{x,y\\}, x \\in H_1 \\land y \\in H_2 \\land x = y \\Rightarrow x = 1 $$$

Lean4

@[to_additive]
theorem disjoint_def' {H₁ H₂ : Subgroup G} : Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x = y → x = 1 :=
  disjoint_def.trans ⟨fun h _x _y hx hy hxy ↦ h hx <| hxy.symm ▸ hy, fun h _x hx hx' ↦ h hx hx' rfl⟩

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