isComplement_iff_existsUnique_mul_inv_mem

English

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

Русский

IsComplement S T эквивалентно: для каждого g существует единственный t ∈ T such that g t⁻¹ ∈ S.

LaTeX

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

Lean4

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

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