exists_isComplement_right — Mathlib

English

For any H and g ∈ G, there exists T with IsComplement H T and g ∈ T.

Русский

Для любой H и элемента g ∈ G существует T, такое что IsComplement H T и g ∈ T.

LaTeX

$$There exists T such that IsComplement H T and g ∈ T.$$

Lean4

@[to_additive]
theorem exists_isComplement_right (H : Subgroup G) (g : G) : ∃ T, IsComplement H T ∧ g ∈ T := by
  classical
  refine
    ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_, Quotient.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

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