mk_out_eq_mul — Mathlib

English

mk_out_eq_mul: There exist h,k with h ∈ H, k ∈ K such that (Quotient.out (DoubleCoset.mk H K g)) = h g k.

Русский

Существуют h ∈ H и k ∈ K такие, что out(Mk H K g) = h g k.

LaTeX

$$$ \\exists h \\in H, \\exists k \\in K : \\mathrm{Quotient.out}(\\mathrm{DoubleCoset.mk}(H,K,g)) = h \\, g \\, k $$$

Lean4

theorem mk_out_eq_mul (H K : Subgroup G) (g : G) :
    ∃ h k : G, h ∈ H ∧ k ∈ K ∧ (mk H K g : Quotient ↑H ↑K).out = h * g * k :=
  by
  have := eq H K (mk H K g : Quotient ↑H ↑K).out g
  rw [out_eq'] at this
  obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
  refine ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq ?_)⟩
  rw [← mul_assoc, ← T]

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