English
For any subgroup H and element g ∈ G, there exists a subset S with IsComplement S H and g ∈ S.
Русский
Для любой подгруппы H и элемента g ∈ G существует подмножество S, такое что IsComplement S H и g ∈ S.
LaTeX
$$There exists S such that IsComplement S H and g ∈ S.$$
Lean4
@[to_additive]
theorem exists_isComplement_left (H : Subgroup G) (g : G) : ∃ S, IsComplement S H ∧ g ∈ S := by
classical
refine
⟨Set.range (Function.update Quotient.out _ g), isComplement_range_left fun q ↦ ?_, QuotientGroup.mk g,
Function.update_self (Quotient.mk'' g) g Quotient.out⟩
by_cases hq : q = Quotient.mk'' g
· exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)
· refine Function.update_of_ne ?_ g Quotient.out ▸ q.out_eq'
exact hq
