English
If K is a nonempty directed set of subgroups, the membership in sSup K is equivalent to there existing a member s ∈ K with x ∈ s.
Русский
Если K — ненулевой направленный набор подгрупп, принадлежность x к sSup K эквивалентна тому, что x принадлежит некоторой подгруппе s ∈ K.
LaTeX
$$$ x \\in sSup K \\iff \\exists s \\in K, x \\in s $$$
Lean4
@[to_additive]
theorem mul_injective_of_disjoint {H₁ H₂ : Subgroup G} (h : Disjoint H₁ H₂) :
Function.Injective (fun g => g.1 * g.2 : H₁ × H₂ → G) :=
by
intro x y hxy
rw [← inv_mul_eq_iff_eq_mul, ← mul_assoc, ← mul_inv_eq_one, mul_assoc] at hxy
replace hxy := disjoint_iff_mul_eq_one.mp h (y.1⁻¹ * x.1).prop (x.2 * y.2⁻¹).prop hxy
rwa [coe_mul, coe_mul, coe_inv, coe_inv, inv_mul_eq_one, mul_inv_eq_one, ← Subtype.ext_iff, ← Subtype.ext_iff,
eq_comm, ← Prod.ext_iff] at hxy
