IsComplement' — Mathlib

English

IsComplement' H K is equivalent to IsComplement (H as a Set) (K as a Set).

Русский

IsComplement' H K эквивалентно IsComplement (H как множество) (K как множество).

LaTeX

$$$ \text{IsComplement'}(H,K) \iff \text{IsComplement}(H \text{ as Set}, K \text{ as Set}). $$$

Lean4

/-- `H` and `K` are complements if `(*) : H × K → G` is a bijection -/
@[to_additive /-- `H` and `K` are complements if `(+) : H × K → G` is a bijection -/
    ]
abbrev IsComplement' :=
  IsComplement (H : Set G) (K : Set G)

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