isComplement'_iff_card_mul_and_disjoint

English

For finite G, IsComplement'(H,K) holds if and only if |H| · |K| = |G| and Disjoint(H,K).

Русский

Для конечной G выполняется: IsComplement'(H,K) тогда и только тогда, когда |H| · |K| = |G| и Disjoint(H,K).

LaTeX

$$IsComplement'(H,K) ↔ (|H| · |K| = |G|) ∧ Disjoint(H,K)$$

Lean4

theorem isComplement'_iff_card_mul_and_disjoint [Finite G] :
    IsComplement' H K ↔ Nat.card H * Nat.card K = Nat.card G ∧ Disjoint H K :=
  ⟨fun h => ⟨h.card_mul, h.disjoint⟩, fun h => isComplement'_of_card_mul_and_disjoint h.1 h.2⟩

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