isComplement_iff_existsUnique_inv_mul_mem

English

IsComplement S T is equivalent to: for every g, there exists a unique s ∈ S with s⁻¹ g ∈ T.

Русский

IsComplement S T эквивалентно: для каждого g существует единично ровно один элемент s ∈ S, удовлетворяющий s⁻¹ g ∈ T.

LaTeX

$$$IsComplement S T \\\\Leftrightarrow \\\\forall g, \\\\exists! s : S, (s : G)^{-1} * g \\\\in T$$$

Lean4

@[to_additive]
theorem isComplement_iff_existsUnique_inv_mul_mem : IsComplement S T ↔ ∀ g, ∃! s : S, (s : G)⁻¹ * g ∈ T :=
  by
  convert isComplement_iff_existsUnique with g
  constructor <;> rintro ⟨x, hx, hx'⟩
  · exact ⟨(x, ⟨_, hx⟩), by simp, by aesop⟩
  · exact ⟨x.1, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (y, ⟨_, hy⟩)).1⟩

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