disjoint_iff_mul_eq_one — Mathlib

English

Disjoint H1 H2 is equivalent to: for all x1 ∈ H1, x2 ∈ H2, if x1 x2 = 1 then x1 = 1 and x2 = 1.

Русский

Не пересечение подгрупп эквивалентно: для любых x1 ∈ H1, x2 ∈ H2, если x1 x2 = 1, то x1 = 1 и x2 = 1.

LaTeX

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

Lean4

@[to_additive]
theorem disjoint_iff_mul_eq_one {H₁ H₂ : Subgroup G} :
    Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1 :=
  disjoint_def'.trans
    ⟨fun h x y hx hy hxy =>
      let hx1 : x = 1 := h hx (H₂.inv_mem hy) (eq_inv_iff_mul_eq_one.mpr hxy)
      ⟨hx1, by simpa [hx1] using hxy⟩,
      fun h _ _ hx hy hxy => (h hx (H₂.inv_mem hy) (mul_inv_eq_one.mpr hxy)).1⟩

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