pairwiseDisjoint_smul — Mathlib

English

If S and T form a complement in G, then the family of left translates {a·T : a ∈ S} is pairwise disjoint; that is, for any a,b ∈ S with a ≠ b, (aT) ∩ (bT) = ∅.

Русский

Если S и T образуют дополнение в группе G, то множество левых переносов {a·T : a ∈ S} попарно непересекаются; то есть для любых a,b ∈ S с a ≠ b выполняется (aT) ∩ (bT) = ∅.

LaTeX

$$$\\\\forall a \\\\in S \\,\\\\forall b \\\\in S, a \\\\neq b \\\to (aT) \\cap (bT) = \\emptyset$$$

Lean4

@[to_additive]
theorem pairwiseDisjoint_smul (hst : IsComplement S T) : S.PairwiseDisjoint (· • T) := fun a ha b hb hab ↦
  disjoint_iff_forall_ne.2 <| by
    rintro _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩
    exact hst.1.ne (a₁ := (⟨a, ha⟩, ⟨c, hc⟩)) (a₂ := (⟨b, hb⟩, ⟨d, hd⟩)) (by simp [hab])

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